This is an old revision of the document!
Homework 06 - Due April 9
Problem 1
(Recall Definition of Resolution for FOL.)
Let denote formula \[
\forall x. (A_1(x) \rightarrow B_1(x)) \land (A_2(x) \rightarrow B_2(x)) \leftrightarrow (A_1(x) \land B_1(x)) \lor (A_2(x) \land B_2(x))
\] For each of the following formulas, if the formula is valid, use resolution to prove it; if it is invalid, construct at least one Herbrand model for its negation.
a): Formula
b): Formula \[ \begin{array}{l}
(\forall y. \lnot (A_1(y) \land A_2(y))) \rightarrow F_0
\end{array} \]
c): Formula \[ \begin{array}{l}
(\forall y. A_1(y) \leftrightarrow \lnot A_2(y)) \rightarrow F_0
\end{array} \]
d): Formula \[ \begin{array}{l}
(\forall y. A_1(y) \leftrightarrow \lnot A_2(y)) \land (\forall z. B_1(z) \leftrightarrow \lnot B_2(z)) \rightarrow F_0
\end{array} \]
e): Formula: \[ \begin{array}{l}
(\forall x. \lnot R(x,x)) \land (\forall x. R(x,f(x)) \rightarrow (\exists x,y,z.\ R(x,y) \land R(y,z) \land \lnot R(x,z))
\end{array} \]
Problem 2
(Recall Sets and Relations.)
We say that a binary relation is a partial order iff it is reflexive, antisymmetric, and transitive. Let be a non-empty set and a binary relation on . Let be the reflexive transitive closure of .
a) Give an example for which is not necessarily a partial order.
b) Define . Show that is a congruence with respect to , that is: is reflexive, symmetric, and transitive and for all , \[
(x,x') \in s \land (y,y') \in s \rightarrow ((x,y) \in r \leftrightarrow (x',y') \in r)
\]
c) For each let . Let . Define a new relation, , by \[
[r] = \{ ([x],[y]) \mid (x,y) \in r \}
\] Show that is a partial order on .
Optional: Explain this constructions using terminology of graphs and strongly connected components.
Problem 3
(Recall Unification.)
Let be an infinite set of variables. Let be some first-order language. We will consider terms that contain variables from and function symbols from .
Following Problem 2 above, let iff there exists substitution such that where is the standard relation composition.
a) Compute . What is its relationship to ?
b) Compute . Show that relation holds iff where is a relation which is bijection on the set .
Optional: c) Let be a fixed set of syntactic equations. Let be the set of unifiers for and . Show that if is non-empty, then there exists such that for all , we have (that is, is the least element of with respect to defined as in Problem 2).