Differences

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

--- sav08:herbrand_s_expansion_theorem [2009/05/26 10:26]
vkuncak
+++ sav08:herbrand_s_expansion_theorem [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Herbrand's Expansion Theorem ======
-===== Expansion of a Clause =====
-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.
-We obtain an instance of a clause $C$ by replacing all variables with some ground terms from $GT$.
-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 formulas whose propositional variables have "long names".
-For an expansion of clause $C_G$ we can construct the corresponding propositional formula $p(C_G)$.
-**Example**
-Let's consider the expanded formula $F=P(f(a)) \wedge R(a, f(a))$, then $p(F)=p_1 \wedge p_4$
-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 = (GT,\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 $(GT,\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 $GT$
-**Example:** Take the first three clauses our example (from [[Normal Forms for First-Order Logic]]):
-  * $R(x,g(x))$
-  * $\neg R(x,y) \lor R(x,f(y,z)))$
-  * $P(x) \lor P(f(x,a))$
-Taking as domain $D$ the set of natural numbers, the structure $(D,\alpha)$ is a model of the conjunction of these three clauses, where $\alpha$ is given by:
-  * $\alpha(a) = 1$
-  * $\alpha(c) = 2$
-  * $\alpha(g)(x) = (x + 1)$
-  * $\alpha(f)(y,z) = y+z$
-  * $\alpha(R) = \{(x,y).\ x < y\}$
-  * $\alpha(P) = \{x.\ x \mbox{ is even} \}$
-This model induces an Herbrand model $(GT,\alpha_H)$, in which $\alpha_H(P)$ is a set of ground terms and $\alpha_H(R)$ is a relation on ground terms, $\alpha_H(R) \subseteq GT^2$.
-To determine, for example, whether $(f(a,a),g(g(a))) \in \alpha_H(R)$ we check the truth value of the formula
-\[
-   R(f(a,a),g(c)))
-\]
-in the original interpretation $(D,\alpha)$. In this case, the formula reduces to $1+1 < 2+1$ and is true in the interpretation. Therefore, we define $\alpha_H(R)$ to contain the pair of ground terms $(f(a,a),g(c)))$.