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.

Example

The clauses ${\displaystyle P(x),Q(x)}$ and ${\displaystyle \neg P(b)}$ can apply this rule with ${\displaystyle [b/x]}$ as unifier.

Here x is a variable and b is a constant.

${\displaystyle {\frac {P(x),Q(x)\,\,\,\,\neg P(b)}{Q(b)}}[b/x]}$

Here we see that

• The clauses ${\displaystyle P(x),Q(x)}$ and ${\displaystyle \neg P(x)}$ are the inference’s premises
• ${\displaystyle Q(b)}$ (the resolvent of the premises) is its conclusion.
• The literal ${\displaystyle P(x)}$ is the left resolved literal,
• The literal ${\displaystyle \neg P(b)}$ is the right resolved literal,
• ${\displaystyle P}$ is the resolved atom or pivot.
• ${\displaystyle [b/x]}$ is the most general unifier of the resolved literals.

Notes

1. Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd International Conference on Automated Deduction, 2011.
2. Enrique P. Arís, Juan L. González y Fernando M. Rubio, Lógica Computacional, Thomson, (2005).