Differences
This shows you the differences between two versions of the page.
| Next revision Both sides next revision | |||
|
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:11] vkuncak created |
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:12] vkuncak |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| \] | \] | ||
| ++++ | ++++ | ||
| + | |||
| + | 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. ++ | By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? ++| Only if formula has no equality. ++ | ||
| + | |||