• 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) Both sides previous revision Previous revision 2009/05/14 13:15 vkuncak 2009/05/14 12:30 vkuncak 2008/04/01 12:08 vkuncak 2008/04/01 12:08 vkuncak created Next revision Previous revision 2009/05/14 13:15 vkuncak 2009/05/14 12:30 vkuncak 2008/04/01 12:08 vkuncak 2008/04/01 12:08 vkuncak created 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.