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

↑ Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd International Conference on Automated Deduction, 2011.
↑ Enrique P. Arís, Juan L. González y Fernando M. Rubio, Lógica Computacional, Thomson, (2005).

This article is issued from Wikipedia - version of the 5/18/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.