LARA

Definition of Resolution for First-Order Logic

This is the definition of resolution rule for first-order logic clauses.

\begin{equation*}
\frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
     {subst(\sigma)(C' \cup D')}
\end{equation*}

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 instantiation followed by resolution.