Speaker: David Mitchell

Title:
Negative Resolution is Weaker than Resolution

Abstract:
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.