Resolution: subsumption, factoring etc

Binary resolution is the core inference rule of a resolution theorem prover, but there are some other things you may choose to do, or you may have to do, to prune the search space of ever-expanding resolvent clauses or to find a proof.

The pictures below are very hand-wavy: to understand what is going on, refer to the three slide sets from Imperial College referenced towards the end of this post.

Note that 'mgu' is 'most general unifier', the list of mappings from variables to other variables or constants which can make two terms identical.

P(a,y,z) and P(x,b,w) unify to P(a,b,w) with mgu = {x → a, y → b, z → w}.


1. Basic Resolution and Factoring

2. Why do we rename clauses?

Because x can't be bound to 2 different things. Rename x in the 2nd clause to y and we're good.


3. Subsumption and Tautology Deletion

Subsumption and factoring are complicated. You can win by removing redundant clauses, lose by the time it takes to do so. Sometimes you have to do it to get a proof. Other times, too much enthusiasm can make a proof impossible. Slides 6 below has more.

Imperial College has long had high-quality material on the theory and design of resolution theorem provers. An excellent set of slides (PDF) can be downloaded from here.

For design and implementation see particularly:

• Slides 3: Unification, Refutation by resolution, Factoring
• Slides 6: Subsumption, Tautology removal, Factoring
• Slides 12: Equality and Resolution: Paramodulation

The directory of this excellent and comprehensive slide set is here.