Differences
This shows you the differences between two versions of the page.
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. | ||