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