Differences

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

--- sav08:non-ground_instantiation_and_resolution [2008/04/01 17:39]
vkuncak
+++ sav08:non-ground_instantiation_and_resolution [2015/04/21 17:30] (current)
@@ Line 5: / Line 5: @@
 Why apply resolution only on ground terms?
 Consider arbitrary clauses $C, D$ and any atom $A$.
-\[
+\begin{equation*}
 \frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}}
      {C \cup D}
-\]
+\end{equation*}
 ++++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)}
      {\forall \vec x.\ \lnot C \rightarrow D}
-\]
+\end{equation*}
 ++++
@@ Line 19: / Line 19: @@
 For arbitrary substitution:
-\[
+\begin{equation*}
 \frac{C}{subst(\sigma)(C)}
-\]
+\end{equation*}
 ++++Is this non-ground instantiation rule sound?|
-\[
+\begin{equation*}
 \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$.)
 ++++
@@ Line 31: / Line 31: @@
 Illustration of rules.
-===== Reducing the Search Space =====
+===== Combining Instantiation and Resolution =====
-More powerful rules.
+These two are more powerful rules.
-But more choices at each step.
+But we therefore have more choices at each step.
 If we try to do the proof, how do we know what to instantiate with? ++|we instantiate to enable subsequent resolution rule.++
-**Resolution with instantiation**
+**Instantiation followed by resolution:**
-\[
+\begin{equation*}
 \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
      {subst(\sigma_1)(C) \cup subst(\sigma_2)(D)}
-\]
+\end{equation*}
 such that $subst(\sigma_1)(A_1) = subst(\sigma_2)(A_2)$.
-Resolution with instantiation generalizes resolution and ground resolution.
+This rule generalizes the above non-ground resolution and ground resolution.
+Note: if we apply instantiation that renames variables in each clause, then $\sigma_1$ and $\sigma_2$ can have disjoint domains and we let $\sigma = \sigma_1 \cup \sigma_2$, obtaining
 One complete proof system contains:
+  * instantiation followed by resolution
   * instantiation
-  * resolution with instantiation
-Note: if we apply instantiation that renames variables in each clause, then $\sigma_1$ and $\sigma_2$ can have disjoint domains and we let $\sigma = \sigma_1 \cup \sigma_2$, obtaining
 Note: $\sigma$ such that $subst(\sigma)(A_1) = subst(\sigma)(A_2)$ is called a **unifier** for $\{A_1,A_2\}$.
-Further step: do we need to consider all unifiers?
+Note: a //renaming// is substitution whose domain and codomain are variables and which is injective.  That, is, it renames variables without clashing variable names.
+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.  To compute it we can use the standard [[Unification]] algorithm.
+To compute it we can use the standard [[Unification]] algorithm.