Resolution inference

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

[math]\displaystyle{ \frac{\Gamma_1 \cup\left\\{ \ell\right\\} \,\,\,\, \Gamma_2 \cup\left\\{ \overline{\ell}\right\\} }{\Gamma_1 \cup\Gamma_2}|\ell| }[/math]

We call:

* The clauses [math]\displaystyle{ \Gamma_1 \cup\left\\{ \ell\right\\} }[/math] and [math]\displaystyle{ \Gamma_2 \cup\left\\{ \overline{\ell}\right\\} }[/math] are the inference’s premises
* [math]\displaystyle{ \Gamma_1 \cup \Gamma_2 }[/math] (the resolvent of the premises) is its conclusion.
* The literal [math]\displaystyle{ \ell }[/math] is the left resolved literal,
* The literal [math]\displaystyle{ \overline{\ell} }[/math] is the right resolved literal,
* [math]\displaystyle{ |\ell| }[/math] is the resolved atom or pivot.

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

[math]\displaystyle{ \frac{\Gamma_1 \cup\left\\{ L_1\right\\} \,\,\,\, \Gamma_2 \cup\left\\{ L_2\right\\} }{ (\Gamma_1 \cup \Gamma_2)\phi } \phi }[/math]

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

## Example

The clauses [math]\displaystyle{ P(x),Q(x) }[/math] and [math]\displaystyle{ \neg P(b) }[/math] can apply this rule with [math]\displaystyle{ [b/x] }[/math] as unifier.

Here x is a variable and b is a constant.

[math]\displaystyle{ \frac{P(x),Q(x) \,\,\,\, \neg P(b)} {Q(b)}[b/x] }[/math]

Here we see that

* The clauses [math]\displaystyle{ P(x),Q(x) }[/math] and [math]\displaystyle{ \neg P(x) }[/math] are the inference’s premises
* [math]\displaystyle{ Q(b) }[/math] (the resolvent of the premises) is its conclusion.
* The literal [math]\displaystyle{ P(x) }[/math] is the left resolved literal,
* The literal [math]\displaystyle{ \neg P(b) }[/math] is the right resolved literal,
* [math]\displaystyle{ P }[/math] is the resolved atom or pivot.
* [math]\displaystyle{ [b/x] }[/math] 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).

0.00

(0 votes)

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Resolution_inference&oldid=69713"