Exponential Lower Bounds for the Length of Resolution Proofs
The resolution calculus is one of the most commonly used methods in theorem proving. For a long time an exponential lower bound for the length of such proofs was sought. In 1985 this was finally proven by Haken.
KeywordsGreedy Algorithm Proof System Partial Assignment Pigeonhole Principle Resolution Step
Unable to display preview. Download preview PDF.