• English only

# Differences

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

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. ++