Resolution inference

In propositional logic, a resolution inference is an instance of the following rule:^[1]

$\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:^[2]

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

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).