# 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] (current) Both sides previous revision Previous revision 2009/05/26 10:28 vkuncak 2009/05/26 10:26 vkuncak 2008/04/01 15:59 giuliano 2008/03/24 11:38 vkuncak 2008/03/24 11:32 vkuncak 2008/03/24 11:24 vkuncak 2008/03/20 12:14 vkuncak created Next revision Previous revision 2009/05/26 10:28 vkuncak 2009/05/26 10:26 vkuncak 2008/04/01 15:59 giuliano 2008/03/24 11:38 vkuncak 2008/03/24 11:32 vkuncak 2008/03/24 11:24 vkuncak 2008/03/20 12:14 vkuncak created Line 8: Line 8: Define ​ Define ​ - $+ \begin{equation*} ​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 \} ​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 \} -$ + \end{equation*} Note that if $C$ is true in $I$, then $expand(C)$ is also true in $I$ ($expand(C)$ is a consequence of $C$). 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: We expand entire set: - $+ \begin{equation*} ​expand(S) = \bigcup_{C \in S} expand(C) ​expand(S) = \bigcup_{C \in S} expand(C) -$ + \end{equation*} Clauses in the expansion have no variables, they are //ground clauses//. Clauses in the expansion have no variables, they are //ground clauses//. Line 31: Line 31: Define propositional model $I_P : V \to \{\it true},{\it false\}$ by Define propositional model $I_P : V \to \{\it true},{\it false\}$ by - $+ \begin{equation*} I_P(p(C_G)) = e_F(C_G)(I) I_P(p(C_G)) = e_F(C_G)(I) -$ + \end{equation*} Let Let - $+ \begin{equation*} ​propExpand(S) = \{ p(C_G) \mid C_G \in expand(S) \} ​propExpand(S) = \{ p(C_G) \mid C_G \in expand(S) \} -$ + \end{equation*} **Lemma:** If $I$ is a model of $S$, then $I_P$ is a model of $propExpand(S)$. **Lemma:** If $I$ is a model of $S$, then $I_P$ is a model of $propExpand(S)$. Line 80: Line 80: 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$. ​ 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 + To determine, for example, whether $(f(a,a),g(c)) \in \alpha_H(R)$ we check the truth value of the formula - $+ \begin{equation*} ​R(f(a,​a),​g(c))) ​R(f(a,​a),​g(c))) -$ + \end{equation*} - 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)))$. + in the original interpretation $(D,​\alpha)$. ​The truth value of the above formula ​in $\alpha$ ​reduces to $1+1 < 2+1$, which is true. Therefore, we define $\alpha_H(R)$ to contain the pair of ground terms $(f(a,​a),​g(c)))$. On the other hand, $R(f(a,​a),​c)$ evaluates to false in $(D,​\alpha)$,​ so we define $\alpha_H(R)$ so that it does not contain the pair $(f(a,a),c)$.