Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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