Differences
This shows you the differences between two versions of the page.
Both sides previous 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 [2009/05/14 12:41] vkuncak |
||
---|---|---|---|
Line 16: | Line 16: | ||
++++ | ++++ | ||
- | 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. ++ | ||