LARA

Differences

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

Link to this comparison view

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)$.