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:non-ground_instantiation_and_resolution [2008/04/02 10:49]
vkuncak
sav08:non-ground_instantiation_and_resolution [2015/04/21 17:30] (current)
Line 5: Line 5:
 Why apply resolution only on ground terms? Why apply resolution only on ground terms?
 Consider arbitrary clauses $C, D$ and any atom $A$. Consider arbitrary clauses $C, D$ and any atom $A$.
-\[+\begin{equation*}
 \frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}} \frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}}
      {C \cup D}      {C \cup D}
-\]+\end{equation*}
 ++++Is this non-ground resolution rule sound?| ++++Is this non-ground resolution rule sound?|
-\[+\begin{equation*}
 \frac{(\forall \vec x.\ (\lnot C) \rightarrow \lnot A)\ \ \ (\forall \vec x. (\lnot A) \rightarrow D)} \frac{(\forall \vec x.\ (\lnot C) \rightarrow \lnot A)\ \ \ (\forall \vec x. (\lnot A) \rightarrow D)}
      ​{\forall \vec x.\ \lnot C \rightarrow D}      ​{\forall \vec x.\ \lnot C \rightarrow D}
-\]+\end{equation*}
 ++++ ++++
  
Line 19: Line 19:
  
 For arbitrary substitution:​ For arbitrary substitution:​
-\[+\begin{equation*}
 \frac{C}{subst(\sigma)(C)} \frac{C}{subst(\sigma)(C)}
-\]+\end{equation*}
 ++++Is this non-ground instantiation rule sound?| ++++Is this non-ground instantiation rule sound?|
-\[+\begin{equation*}
 \frac{\forall \vec x.\ C}{\forall \vec x.\ subst(\sigma)(C)} \frac{\forall \vec x.\ C}{\forall \vec x.\ subst(\sigma)(C)}
-\]+\end{equation*}
 (Here $\vec x$ contains both variables in domain and in range of $\sigma$.) (Here $\vec x$ contains both variables in domain and in range of $\sigma$.)
 ++++ ++++
Line 40: Line 40:
  
 **Instantiation followed by resolution:​** **Instantiation followed by resolution:​**
-\[+\begin{equation*}
 \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
      ​{subst(\sigma_1)(C) \cup subst(\sigma_2)(D)}      ​{subst(\sigma_1)(C) \cup subst(\sigma_2)(D)}
-\]+\end{equation*}
 such that $subst(\sigma_1)(A_1) = subst(\sigma_2)(A_2)$. such that $subst(\sigma_1)(A_1) = subst(\sigma_2)(A_2)$.
  
Line 60: Line 60:
 Further step: do we need to consider all possible unifiers? Further step: do we need to consider all possible unifiers?
  
-Most general unifier for $\{A_1,​A_2\}$,​ denoted $mgu(A_1,​A_2)$+Most general unifier for $\{A_1,​A_2\}$,​ denoted $mgu(A_1,​A_2)$.
  
 To compute it we can use the standard [[Unification]] algorithm. To compute it we can use the standard [[Unification]] algorithm.
  
 
sav08/non-ground_instantiation_and_resolution.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice