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 $\phi$ is a most general unifier of $L_{1}$ and ${\overline {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.