Date: March 18, 2003
Time: 12:00pm - 1:00pm
Place: ASB 9705

Speaker: David Mitchell

Negative Resolution is Weaker than Resolution

Effectively use a proof system in a theorem prover or other solver requires finding an good strategy for applying derivation rules, and this has lead to use of a variety of restricted forms of resolution.While such restrictions simplify the task of designing a strategy, they also may be less powerful than unrestricted resolution.

We will illustrate by showing how to obtain an exponential separation between negative resolution and unrestricted resolution. That is, we will exhibit a family of formulas and show that they have short resolution proofs, but negative resolution proofs only of exponential length.