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]
Line 1: Line 1:
-====== Herbrand Model and Unsat Proof for an Example ====== 
- 
-We will look at the language ${\cal L} = \{P, R, a, f\}$ where 
-  * $P$ is relation symbol of arity one 
-  * $R$ is relation symbol of arity two 
-  * $a$ is a constant 
-  * $f$ is a function symbol of two arguments 
- 
-Consider this formula in ${\cal L}$: 
-\[ 
-\begin{array}{l@{}l} 
-  & (\forall x. \exists y.\ R(x,y))\ \land \\ 
-      & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,​f(y,​z)))\ \land \\ 
-      & (\forall x.\ P(x) \lor P(f(x,a)))\ \\ 
-      & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) 
-\end{array} 
-\] 
-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{array}{l@{}l} 
-\lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ 
-      & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,​f(y,​z)))\ \land \\ 
-      & (\forall x.\ P(x) \lor P(f(x,a)))\ \big)\\ 
-      & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg) 
-\end{array} 
-\] 
- 
-Parsing the formula. 
- 
-Negation normal form. 
- 
-Skolem normal form for each clause. 
- 
-Herbrand universe. 
- 
-Propositional expansion. 
- 
-Propositional proof. 
- 
-Recovering first-order proof from propositional proof.