Lab for Automated Reasoning and Analysis LARA

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