• 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) Both sides previous revision Previous revision 2008/04/02 10:50 vkuncak 2008/04/02 10:49 vkuncak 2008/04/01 20:09 vkuncak 2008/04/01 20:08 vkuncak 2008/04/01 17:45 vkuncak 2008/04/01 17:39 vkuncak 2008/04/01 17:05 vkuncak 2008/04/01 16:43 vkuncak 2008/04/01 16:34 vkuncak 2008/04/01 16:25 vkuncak 2008/04/01 16:21 vkuncak 2008/04/01 16:21 vkuncak 2008/04/01 16:14 vkuncak 2008/04/01 16:09 vkuncak 2008/04/01 16:00 vkuncak created Next revision Previous revision 2008/04/02 10:50 vkuncak 2008/04/02 10:49 vkuncak 2008/04/01 20:09 vkuncak 2008/04/01 20:08 vkuncak 2008/04/01 17:45 vkuncak 2008/04/01 17:39 vkuncak 2008/04/01 17:05 vkuncak 2008/04/01 16:43 vkuncak 2008/04/01 16:34 vkuncak 2008/04/01 16:25 vkuncak 2008/04/01 16:21 vkuncak 2008/04/01 16:21 vkuncak 2008/04/01 16:14 vkuncak 2008/04/01 16:09 vkuncak 2008/04/01 16:00 vkuncak created 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.