Resolution inference

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

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

We call:

• The clauses $\Gamma _{1}\cup \left\{\ell \right\}$ and $\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}$ are the inference’s premises

• $\Gamma _{1}\cup \Gamma _{2}$ (the resolvent of the premises) is its conclusion.

• The literal $\ell$ is the left resolved literal,

• The literal ${\overline {\ell }}$ is the right resolved literal,

• $|\ell |$ is the resolved atom or pivot.

This rule can be generalized to first-order logic to:

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

where $L_{1}$ and $L_{2}$ are of different sign, $\phi$ is a most general unifier of $L_{1}$ and $L_{2}$ and $\Gamma _{1}$ and $\Gamma _{2}$ have no common variables.

Example

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

Here x is a variable and B is a constant.

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

Here we see that

• The clauses $P(x),Q(x)$ and $\neg P(x)$ are the inference’s premises

• $Q(B)$ (the resolvent of the premises) is its conclusion.

• The literal $P(x)$ is the left resolved literal,

• The literal $\neg P(B)$ is the right resolved literal,

• $P$ is the resolved atom or pivot.

• $[B/x]$ is the most general unifier of the resolved literals.