Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:herbrand_s_expansion_theorem [2009/05/26 10:28] 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 81: | Line 81: | ||
To determine, for example, whether $(f(a,a),g(c)) \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)$. 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)$. | 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)$. | ||