• English only

Differences

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

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.