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.