Resolution inference

In propositional logic, a resolution inference is an instance of the following rule:[1]

${\displaystyle {\frac {\Gamma _{1}\cup \left\{\ell \right\}\,\,\,\,\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}{\Gamma _{1}\cup \Gamma _{2}}}|\ell |}$

We call:

• The clauses ${\displaystyle \Gamma _{1}\cup \left\{\ell \right\}}$ and ${\displaystyle \Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}$ are the inference’s premises
• ${\displaystyle \Gamma _{1}\cup \Gamma _{2}}$ (the resolvent of the premises) is its conclusion.
• The literal ${\displaystyle \ell }$ is the left resolved literal,
• The literal ${\displaystyle {\overline {\ell }}}$ is the right resolved literal,
• ${\displaystyle |\ell |}$ is the resolved atom or pivot.

This rule can be generalized to first-order logic to:[2]

${\displaystyle {\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2}\right\}}{(\Gamma _{1}\cup \Gamma _{2})\phi }}\phi }$

where ${\displaystyle \phi }$ is a most general unifier of ${\displaystyle L_{1}}$ and ${\displaystyle {\overline {L_{2}}}}$ and ${\displaystyle \Gamma _{1}}$ and ${\displaystyle \Gamma _{2}}$ have no common variables.