• English only

Differences

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

Link to this comparison view

sav08:herbrand_s_expansion_theorem [2009/05/26 10:26]
vkuncak
sav08:herbrand_s_expansion_theorem [2015/04/21 17:30] (current)
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)$.

sav08/herbrand_s_expansion_theorem.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice