Resolution inference

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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[edit]

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[edit]

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