Resolution inference

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

$\frac{{\mathrm{\Gamma }}_1\cup \left\{\ell \right\}{\mathrm{\Gamma }}_2\cup \left\{\bar{\ell }\right\}}{{\mathrm{\Gamma }}_1\cup {\mathrm{\Gamma }}_2}|\ell |$

We call:

• The clauses ${\mathrm{\Gamma }}_1\cup \left\{\ell \right\}$ and ${\mathrm{\Gamma }}_2\cup \left\{\bar{\ell }\right\}$ are the inference’s premises
• ${\mathrm{\Gamma }}_1\cup {\mathrm{\Gamma }}_2$ (the resolvent of the premises) is its conclusion.
• The literal $\ell$ is the left resolved literal,
• The literal $\bar{\ell }$ is the right resolved literal,
• $|\ell |$ is the resolved atom or pivot.

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

$\frac{{\mathrm{\Gamma }}_1\cup \left\{L_1\right\}{\mathrm{\Gamma }}_2\cup \left\{L_2\right\}}{({\mathrm{\Gamma }}_1\cup {\mathrm{\Gamma }}_2)\varphi }\varphi$

where $\varphi$ is a most general unifier of $L_1$ and $\overline{L_2}$ and ${\mathrm{\Gamma }}_1$ and ${\mathrm{\Gamma }}_2$ have no common variables.

Example

The clauses $P(x),Q(x)$ and $\mathrm{\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)\mathrm{\neg }P(b)}{Q(b)}[b/x]$

Here we see that

• The clauses $P(x),Q(x)$ and $\mathrm{\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 $\mathrm{\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.