Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:homework06 [2008/04/08 15:45] vkuncak |
sav08:homework06 [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 6: | Line 6: | ||
Let $F_0$ denote formula | Let $F_0$ denote formula | ||
- | \[ | + | \begin{equation*} |
\forall x. (A_1(x) \rightarrow B_1(x)) \land (A_2(x) \rightarrow B_2(x)) \leftrightarrow | \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)) | (A_1(x) \land B_1(x)) \lor (A_2(x) \land B_2(x)) | ||
- | \] | + | \end{equation*} |
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. | 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. | ||
Line 15: | Line 15: | ||
**b):** Formula | **b):** Formula | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
(\forall y. \lnot (A_1(y) \land A_2(y))) \rightarrow F_0 | (\forall y. \lnot (A_1(y) \land A_2(y))) \rightarrow F_0 | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
**c):** Formula | **c):** Formula | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
(\forall y. A_1(y) \leftrightarrow \lnot A_2(y)) \rightarrow F_0 | (\forall y. A_1(y) \leftrightarrow \lnot A_2(y)) \rightarrow F_0 | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
**d):** Formula | **d):** Formula | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \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 | (\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} | \end{array} | ||
- | \] | + | \end{equation*} |
**e):** Formula: | **e):** Formula: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \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)) | (\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} | \end{array} | ||
- | \] | + | \end{equation*} |
===== Problem 2 ===== | ===== Problem 2 ===== | ||
Line 51: | Line 51: | ||
**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$, | **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$, | ||
- | \[ | + | \begin{equation*} |
(x,x') \in s \land (y,y') \in s \rightarrow ((x,y) \in r \leftrightarrow (x',y') \in r) | (x,x') \in s \land (y,y') \in s \rightarrow ((x,y) \in r \leftrightarrow (x',y') \in r) | ||
- | \] | + | \end{equation*} |
**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 | **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 | ||
- | \[ | + | \begin{equation*} |
[r] = \{ ([x],[y]) \mid (x,y) \in r \} | [r] = \{ ([x],[y]) \mid (x,y) \in r \} | ||
- | \] | + | \end{equation*} |
Show that $[r]$ is a partial order on $[D]$. | Show that $[r]$ is a partial order on $[D]$. | ||
Line 65: | Line 65: | ||
===== Problem 3 ===== | ===== Problem 3 ===== | ||
- | (Recall [[Unification]].) | + | (Recall [[Substitutions for First-Order Logic]], [[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}$. | 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}$. |