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: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