Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:herbrand_model_for_an_example [2009/05/14 12:30]
vkuncak
sav08:herbrand_model_for_an_example [2015/04/21 17:30] (current)
Line 1: Line 1:
 ====== Herbrand Model and Unsat Proof for an Example ====== ====== Herbrand Model and Unsat Proof for an Example ======
 +
 +[[wp>​Herbrand]]
  
 We will look at the language ${\cal L} = \{P, R, a, f\}$ where We will look at the language ${\cal L} = \{P, R, a, f\}$ where
Line 8: Line 10:
  
 Consider this formula in ${\cal L}$: Consider this formula in ${\cal L}$:
-\[+\begin{equation*}
 \begin{array}{l@{}l} \begin{array}{l@{}l}
   & (\forall x. \exists y.\ R(x,y))\ \land \\   & (\forall x. \exists y.\ R(x,y))\ \land \\
Line 15: Line 17:
       & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y)       & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y)
 \end{array} \end{array}
-\]+\end{equation*}
 We are interested in checking the //​validity//​ of this formula (is it true in all interpretations). ​ We will check the //​satisfiability//​ of the negation of this formula (does it have a model): ​ We are interested in checking the //​validity//​ of this formula (is it true in all interpretations). ​ We will check the //​satisfiability//​ of the negation of this formula (does it have a model): ​
-\[+\begin{equation*}
 \begin{array}{l@{}l} \begin{array}{l@{}l}
 \lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ \lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\
Line 24: Line 26:
       & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg)       & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg)
 \end{array} \end{array}
-\]+\end{equation*}
  
 Parsing the formula. Parsing the formula.
 
sav08/herbrand_model_for_an_example.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice