LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:14]
vkuncak
sav08:finite_model_and_infinite_herbrand_model_example [2009/05/14 12:41]
vkuncak
Line 10: Line 10:
 What are possible cardinalities for models? ++| they all have exactly two elements.++ What are possible cardinalities for models? ++| they all have exactly two elements.++
  
-What is Herbrand model for this formula? ++++|+What are ground terms for this formula? ++++|
 \[ \[
     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 \}
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. ++