Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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}$.
 
sav08/homework06.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice