Differences
This shows you the differences between two versions of the page.
sav08:herbrand_s_expansion_theorem [2008/04/01 15:59] giuliano |
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$ | ||