Differences

This shows you the differences between two versions of the page.

--- sav08:homework06 [2008/04/08 15:45]
vkuncak
+++ sav08:homework06 [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Homework 06 - Due April 9 ======
-===== Problem 1 =====
-(Recall [[Definition of Resolution for FOL]].)
-Let $F_0$ 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 $F_0$
-**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 $D$ be a non-empty set and $r_0 \subseteq D \times D$ a binary relation on $D$.  Let $r = r_0^* = \bigcup_{i\ge 0} r_0^n$ be the reflexive transitive closure of $r_0$.
-**a)** Give an example $r_0$ for which $r$ is not necessarily a partial order.
-**b)** Define $s = r \cap r^{-1}$.  Show that $s$ is a congruence with respect to $r$, that is: $s$ is reflexive, symmetric, and transitive and for all $x,x',y,y' \in D$,
-\[
-    (x,x') \in s \land (y,y') \in s \rightarrow ((x,y) \in r \leftrightarrow (x',y') \in r)
-\]
-**c)** For each $x \in D$ let $[x] = \{ y \mid (x,y) \in s \}$.  Let $[D] = \{ [x] \mid x \in D\}$.  Define a new relation, $[r] \subseteq [D] \times [D]$, by
-\[
-    [r] = \{ ([x],[y]) \mid (x,y) \in r \}
-\]
-Show that $[r]$ is a partial order on $[D]$.
-Optional: Explain this constructions using terminology of graphs and strongly connected components.
-===== Problem 3 =====
-(Recall [[Unification]].)
-Let $V$ be an infinite set of variables. Let ${\cal L}$ be some first-order language.  We will consider terms that contain variables from $V$ and function symbols from ${\cal L}$.
-Following Problem 2 above, let $(\sigma_1,\sigma_2) \in r_0$ iff there exists substitution $\tau$ such that $subst(\sigma_2) = subst(\sigma_1) \circ subst(\tau)$ where $\circ$ is the standard relation composition.
-**a)** Compute $r = r_0^*$.  What is its relationship to $r_0$?
-**b)** Compute $s = r \cap r^{-1}$.  Show that relation $s$ holds iff $subst(\sigma_2) = subst(\sigma_1) \circ subst(b)$ where $b$ is a relation which is bijection on the set $V$.
-Optional: **c)** Let $E$ be a fixed set of syntactic equations.  Let $U$ be the set of unifiers for $E$ and $[U] = \{ [\sigma] \mid \sigma \in U \}$.  Show that if $U$ is non-empty, then there exists $a \in [U]$ such that for all $b \in [U]$, we have $(a,b) \in [r]$ (that is, $a$ is the least element of $[U]$ with respect to $[r]$ defined as in Problem 2).