This is an old revision of the document!
Definition of Resolution for First-Order Logic
This is the definition of resolution rule for first-order logic clauses. \[ \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}}
{subst(\sigma)(C' \cup D')}
\] where is renaming of , where is renaming of , and where .
We will call the above rule mgu-resolution if we need to differentiate it from instantiation followed by resolution.