• English only

# 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)
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_2are 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]].