Resolution inference

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

${\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 $\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:

${\displaystyle {\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 $L_{2}$ and $\Gamma _{1}$ and $\Gamma _{2}$ share 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.

${\displaystyle {\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.