# Differences

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

 sav08:definition_of_resolution_for_fol [2008/04/01 18:19]vkuncak sav08:definition_of_resolution_for_fol [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/04/02 10:59 vkuncak 2008/04/01 18:19 vkuncak 2008/04/01 18:11 vkuncak created Next revision Previous revision 2008/04/02 10:59 vkuncak 2008/04/01 18:19 vkuncak 2008/04/01 18:11 vkuncak created Line 2: Line 2: This is the definition of resolution rule for first-order logic clauses. This is the definition of resolution rule for first-order logic clauses. - $+ \begin{equation*} \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} ​{subst(\sigma)(C'​ \cup D')} ​{subst(\sigma)(C'​ \cup D')} -$ + \end{equation*} - where $C'$ is renaming of $C$, where $D'$ is renaming of $D$, and where $\sigma = mgu(\{C'​,D'\})$. + where $\sigma_1$, $\sigma_2$ are renamings, $\sigma = mgu(\{subst(\sigma_1)(A_1),​subst(\sigma_2)(A_2)\})$,​ + where $C' ​= subst(\sigma_1)(C)$ and $D' ​= subst(\sigma_2)(D)$. We will call the above rule //​mgu-resolution//​ if we need to differentiate it from [[Non-Ground Instantiation and Resolution|instantiation followed by resolution]]. We will call the above rule //​mgu-resolution//​ if we need to differentiate it from [[Non-Ground Instantiation and Resolution|instantiation followed by resolution]].