# Resolution inference

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

$\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 $\displaystyle{ \Gamma_1 \cup\left\{ \ell\right\} }$ and $\displaystyle{ \Gamma_2 \cup\left\{ \overline{\ell}\right\} }$ are the inference’s premises
• $\displaystyle{ \Gamma_1 \cup \Gamma_2 }$ (the resolvent of the premises) is its conclusion.
• The literal $\displaystyle{ \ell }$ is the left resolved literal,
• The literal $\displaystyle{ \overline{\ell} }$ is the right resolved literal,
• $\displaystyle{ |\ell| }$ is the resolved atom or pivot.

This rule can be generalized to first-order logic to:[2]

$\displaystyle{ \frac{\Gamma_1 \cup\left\{ L_1\right\} \,\,\,\, \Gamma_2 \cup\left\{ L_2\right\} }{ (\Gamma_1 \cup \Gamma_2)\phi } \phi }$

where $\displaystyle{ \phi }$ is a most general unifier of $\displaystyle{ L_1 }$ and $\displaystyle{ \overline{L_2} }$ and $\displaystyle{ \Gamma_1 }$ and $\displaystyle{ \Gamma_2 }$ have no common variables.

## Example

The clauses $\displaystyle{ P(x),Q(x) }$ and $\displaystyle{ \neg P(b) }$ can apply this rule with $\displaystyle{ [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 $\displaystyle{ P(x),Q(x) }$ and $\displaystyle{ \neg P(x) }$ are the inference’s premises
• $\displaystyle{ Q(b) }$ (the resolvent of the premises) is its conclusion.
• The literal $\displaystyle{ P(x) }$ is the left resolved literal,
• The literal $\displaystyle{ \neg P(b) }$ is the right resolved literal,
• $\displaystyle{ P }$ is the resolved atom or pivot.
• $\displaystyle{ [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).