Differences

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

--- sav08:non-ground_instantiation_and_resolution [2008/04/01 16:09]
vkuncak
+++ sav08:non-ground_instantiation_and_resolution [2008/04/01 17:05]
vkuncak
@@ Line 15: / Line 15: @@
 \]
 ++++
-===== Non-Ground Factoring ====
-\[
-\frac{C \cup \{\lnot A,A\}}
-     {C}
-\]
 ===== Non-Ground Instantiation ====
@@ Line 46: / Line 39: @@
 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:
+**Resolution with instantiation**
 \[
 \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
-     {subst(\sigma,C \cup D)}
+     {subst(\sigma_1)(C) \cup subst(\sigma_2)(D)}
 \]
-such that $subst(\sigma,A_1) = subst(\sigma,A_2)$.
+such that $subst(\sigma_1)(A_1) = subst(\sigma_2)(A_2)$.
-Note: $\sigma$ such that $subst(\sigma,A_1) = subst(\sigma,A_2)$ is called a **unifier** for $\{A_1,A_2\}$.
+Resolution with instantiation generalizes resolution and ground resolution.
-Does resolution with instantiation subsume:
+One complete proof system contains:
-  * ++non-ground resolution rule?|yes, take empty substitution++
+  * instantiation
-  * ++instantiation rule?|not by itself++
+  * 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?
-Most general unifier.
+Most general unifier.  To compute it we can use the standard [[Unification]] algorithm.
+----
+**Factoring with instantiation**
+\[
+\frac{C \cup \{A_1, A_2\}}
+     {subst(\sigma)(C)}
+\]
+where $subst(\sigma)(A_1)=subst(\sigma)(A_2)$.