LARA

This is an old revision of the document!

Definition of Resolution for First-Order Logic

\[ \frac{C \cup \{\lnot A_1\}\ \ \ D \cup \{A_2\}} 

   {subst(\sigma)(C' \cup D')}

\] where $C'$ is renaming of $C$, where $D'$ is renaming of $D$, and where $\sigma = mgu(\{C',D'\})$.