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.