Resolution inference

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

Γ1∪{ℓ}Γ2∪{ℓ‾}Γ1∪Γ2|ℓ|

We call:

* The clauses Γ1∪{ℓ} and Γ2∪{ℓ‾} are the inference’s premises
* Γ1∪Γ2 (the resolvent of the premises) is its conclusion.
* The literal ℓ is the left resolved literal,
* The literal ℓ‾ is the right resolved literal,
* |ℓ| is the resolved atom or pivot.

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

Γ1∪{L1}Γ2∪{L2}(Γ1∪Γ2)ϕϕ

where ϕ is a most general unifier of L1 and L2‾ and Γ1 and Γ2 have no common variables.

## Example

The clauses P(x),Q(x) and ¬P(b) can apply this rule with [b/x] as unifier.

Here x is a variable and b is a constant.

P(x),Q(x)¬P(b)Q(b)[b/x]

Here we see that

* The clauses P(x),Q(x) and ¬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 ¬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).

0.00

(0 votes)

|

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