Exponential Lower Bounds for the Length of Resolution Proofs

  • Uwe Schöning
  • Randall Pruim


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.


Greedy Algorithm Proof System Partial Assignment Pigeonhole Principle Resolution Step 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. S. Cook, R. Reckhow: The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44 (1979), 36–50.MathSciNetzbMATHCrossRefGoogle Scholar
  2. A. Haken: The Intractability of Resolution, Theoretical Computer Science 39 (1985), 297–308.MathSciNetzbMATHCrossRefGoogle Scholar
  3. S. Cook and T. Pitassi: A Feasible Constructive Lower Bound for Resolution Proofs, Information Processing Letters 34 (1990), 81–85.MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Uwe Schöning
    • 1
  • Randall Pruim
    • 2
  1. 1.Abt. Theoretische InformatikUniversität UlmUlmGermany
  2. 2.Dept. of Mathematics and StatisticsCalvin CollegeGrand RapidsUSA

Personalised recommendations