Differences
This shows you the differences between two versions of the page.
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:12] vkuncak |
sav08:finite_model_and_infinite_herbrand_model_example [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Formulas with Finite Model but Infinite Herbrand Model ====== | ||
- | |||
- | Example: | ||
- | \[ | ||
- | P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b) | ||
- | \] | ||
- | |||
- | Is this formula satisfiable? ++| yes++ | ||
- | |||
- | What are possible cardinalities for models? ++| they all have exactly two elements.++ | ||
- | |||
- | What is Herbrand model for this formula? ++++| | ||
- | \[ | ||
- | GT = \{ a, b, f(a), f(b), f(f(a)), f(f(b)), \ldots \} | ||
- | \] | ||
- | ++++ | ||
- | |||
- | Cardinality of Herbrand model is ++|infinite!++ | ||
- | |||
- | By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? ++| Only if formula has no equality. ++ | ||
- | |||