Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
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. ++ | ||