• English only

Differences

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

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.