• English only

# 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] (current) Both sides previous revision Previous revision 2008/04/08 15:50 vkuncak 2008/04/08 15:45 vkuncak 2008/04/08 15:38 vkuncak 2008/04/03 13:51 vkuncak 2008/04/02 18:33 vkuncak 2008/04/02 16:59 vkuncak 2008/04/02 16:50 vkuncak 2008/04/02 16:49 vkuncak 2008/04/02 16:47 vkuncak 2008/04/02 16:46 vkuncak 2008/04/02 16:34 vkuncak 2008/04/02 16:27 vkuncak 2008/03/31 20:12 vkuncak 2008/03/31 20:11 vkuncak 2008/03/31 20:11 vkuncak 2008/03/31 19:41 vkuncak 2008/03/31 19:40 vkuncak 2008/03/31 19:39 vkuncak 2008/03/31 19:37 vkuncak 2008/03/31 19:28 vkuncak 2008/03/20 19:23 vkuncak created Next revision Previous revision 2008/04/08 15:50 vkuncak 2008/04/08 15:45 vkuncak 2008/04/08 15:38 vkuncak 2008/04/03 13:51 vkuncak 2008/04/02 18:33 vkuncak 2008/04/02 16:59 vkuncak 2008/04/02 16:50 vkuncak 2008/04/02 16:49 vkuncak 2008/04/02 16:47 vkuncak 2008/04/02 16:46 vkuncak 2008/04/02 16:34 vkuncak 2008/04/02 16:27 vkuncak 2008/03/31 20:12 vkuncak 2008/03/31 20:11 vkuncak 2008/03/31 20:11 vkuncak 2008/03/31 19:41 vkuncak 2008/03/31 19:40 vkuncak 2008/03/31 19:39 vkuncak 2008/03/31 19:37 vkuncak 2008/03/31 19:28 vkuncak 2008/03/20 19:23 vkuncak created 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}$.

sav08/homework06.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice