Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_lecture_6_skeleton [2007/03/30 19:57] vkuncak |
sav07_lecture_6_skeleton [2007/03/30 19:57] vkuncak |
||
---|---|---|---|
Line 25: | Line 25: | ||
We typically do not write universal quantifiers either, because we know that all variables in a clause are universally quantified. | We typically do not write universal quantifiers either, because we know that all variables in a clause are universally quantified. | ||
+ | |||
Line 54: | Line 55: | ||
**Herbrand's theorem**: If a set of clauses in language L is true in some interpretation with domain D, then it is true in an interpretation with domain Term(L). | **Herbrand's theorem**: If a set of clauses in language L is true in some interpretation with domain D, then it is true in an interpretation with domain Term(L). | ||
+ | |||
**Proof sketch**: If set $S$ of clauses is true in interpretation $e$, then define interpretation $e_T$ with domain Term(L) by evaluating functions as in the term model $[[f]](t_1,t_2) = f(t_1,t_2)$, and defining the value of relations by $[[R]]e_T = \{(t_1,t_2)\mid [[R(t_1,t_2)]]e = \mbox{true} \}$ (end of sketch). | **Proof sketch**: If set $S$ of clauses is true in interpretation $e$, then define interpretation $e_T$ with domain Term(L) by evaluating functions as in the term model $[[f]](t_1,t_2) = f(t_1,t_2)$, and defining the value of relations by $[[R]]e_T = \{(t_1,t_2)\mid [[R(t_1,t_2)]]e = \mbox{true} \}$ (end of sketch). | ||