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:finite_model_and_infinite_herbrand_model_example [2009/05/14 12:40]
vkuncak
sav08:finite_model_and_infinite_herbrand_model_example [2015/04/21 17:30] (current)
Line 2: Line 2:
  
 Example: Example:
-\[+\begin{equation*}
     P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)     P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)
-\]+\end{equation*}
  
 Is this formula satisfiable?​ ++| yes++ Is this formula satisfiable?​ ++| yes++
Line 11: Line 11:
  
 What are ground terms for this formula? ++++| What are ground terms for this formula? ++++|
-\[+\begin{equation*}
     GT = \{ a, b, f(a), f(b), f(f(a)), f(f(b)), \ldots \}     GT = \{ a, b, f(a), f(b), f(f(a)), f(f(b)), \ldots \}
-\]+\end{equation*}
 ++++ ++++
  
-Cardinality ​of Herbrand model is ++|infinite!+++Cardinality is ++|infinite!++
  
 By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? ++| Only if formula has no equality! ​ We made this assumption when proving Herbrand theorem. ++ By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? ++| Only if formula has no equality! ​ We made this assumption when proving Herbrand theorem. ++
  
  
 
sav08/finite_model_and_infinite_herbrand_model_example.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice