This is an old revision of the document!
Homework 06 - Due April 9
Problem 1
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
.
c) Let be a fixed set of syntactic equations. Let
be the set of unifiers for
and
. Show that if
is non-empty,
such that for all
, we have
(that is,
is the least element of
).