Differences

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

--- sav08:ground_terms [2008/03/20 12:14]
vkuncak
+++ sav08:ground_terms [2008/04/01 15:55]
giuliano
@@ Line 9: / Line 9: @@
 i.e. built from constants using function symbols.
-**Example**
+**Example**\\
+${\cal L}=\{a, f_1\}$ \\
+$GT=\{a, f(a), f(f(a)), f(f(f(a))), ...\}$
 If ${\cal L}$ has no constants then $GT$ is empty.  In that case, we add a fresh constant $a_0$ into the language and consider ${\cal L} \cup \{a_0\}$ that has a non-empty $GT$.  We call the set $GT$ Herbrand Universe.
@@ Line 23: / Line 25: @@
 $\alpha_H(f)(t_1,\ldots,t_n) =$ ++| $f(t_1,\ldots,t_n)$++
-This defines $\alpha_H(f)$.  How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$?
+This defines $\alpha_H(f)$.  How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$?\\
-  * is this possible for arbitrary set?
+Partition $GT^n$ in two sets, one over which $\alpha_H(R)(t_1,...,t_n)$ is true and the other over which it is false.
+  * is this possible for arbitrary set? ++| no ++
 **Example**
+Consider a set that is not satisfiable : $\{P(a),\ \neg P(a)\}$
 ===== Ground Atoms =====
@@ Line 41: / Line 45: @@
 We will write $p(A)$.
-**Example**
+**Example**\\
+${\cal L}=\{a, f_1, P_1, R_2\}$ \\
-===== Expansion of a Clause =====
+$GT=\{a, f(a), f(f(a)), f(f(f(a))), ...\}$\\
+$HA=\{P(a), R(a,a), P(f(a)), R(a, f(a)), ...\}$\\
-Recall that we do not write quantifiers in the clause, but when we say that a clause is true in a model we mean that its universal closure is true.
+$V=\{p_1, p_2, p_3, p_4, ...\}$\\
+We define p such that :\\
-We obtain an instance of a clause $C$ by replacing all variables with some ground terms from $GT$.
+$p(P(a))=p_1,\ p(R(a,a))=p_2,\ p(P(f(a)))=p_3,\ p(R(a, f(a)))=p_4,...$
-Define
-\[
-   expand(C) = \{ subst(\{x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\})(C) \mid FV(C) = \{x_1,\ldots,x_n\}\ \land\ t_1,\ldots,t_n \in GT \}
-\]
-Note that if $C$ is true in $I$, then $expand(C)$ is also true in $I$ ($expand(C)$ is a consequence of $C$).
-We expand entire set:
-\[
-   expand(S) = \bigcup_{C \in S} expand(C)
-\]
-Clauses in the expansion have no variables, they are //ground clauses//.
-===== Constructing a Propositional Model =====
-We can view the set $expand(S)$ as a set of propositional variables with "long names".
-For an expansion of clause $C_G$ we can construct the corresponding propositional formula $p(C_G)$.
-**Example**
-Define propositional model $I_P : V \to \{{\it true},{\it false\}\}$ by
-\[
-    I_P(p(C_G)) = e_F(C_G)(I)
-\]
-Let
-\[
-   propExpand(S) = \{ p(C_G) \mid C_G \in expand(S) \}
-\]
-**Lemma:** If $I$ is a model of $S$, then $I_P$ is a model of $propExpand(S)$.
-Instead of searching for a model, we can search for a propositional model.
-If we prove there is no propositional model for $propExpand(S)$, then there is no model for $I$.
-What if there is a model $propExpand(S)$?  Could it still be the case that $S$ is unsatisfiable?
-===== Constructing Herbrand Model =====
-For $I = (HU,\alpha_H)$ we define $\alpha_H(R)$ so that $I_H$ evaluates ground formulas $expand(S)$ same as in $I_P$ (and thus same as in $I$).
-We ensure that atomic formulas evaluate the same:
-$   \alpha_H(R) = \{ (t_1,\ldots,t_n)\ \mid $ ++| $I_P(p(R(t_1,\ldots,t_n))) \}$++
-How does it evaluate non-ground formulas?
-**Lemma:** If $I_P$ is a model for $propExpand(S)$, then $(HU,\alpha_H)$ is a model for $S$.
-===== Herbrand's Theorem =====
-**Theorem:** The following statements are equivalent:
-  * set $S$ has a model
-  * set $propExpand(S)$ has a propositional model
-  * set $S$ has a model with domain $HU$