Skip to main content
SpringerLink
Log in
Book cover

Computational Logic pp 127–178Cite as

Propositional Proof Complexity an Introduction

  • Conference paper

Part of the book series: NATO ASI Series ((NATO ASI F,volume 165))

Abstract

This article is an abridged and revised version of a 1996 McGill University technical report [15]. The technical report was based on lectures delivered by the author at a workshop in Holetown, Barbados and on the authors prepared overhead transparencies. The audience at this workshop wrote scribe notes which then formed the technical report [15]. The material selected for the present article corresponds roughly to the content of the author’s lectures at the NATO summer school held in Marktoberdorf, Germany in July-August 1997.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. AjtaiThe complexity of the pigeonhole principlein Proceedings of the 29-th Annual IEEE Symposium on Foundations of Computer Science, 1988, pp. 346–355.

    Google Scholar 

  2. B. Alon and R. BoppanaThe monotone circuit complexity of Boolean functionsCombinatorica, 7 (1987), pp. 1–22.

    Article  MathSciNet  MATH  Google Scholar 

  3. M. L. BonetThe Lengths of Propositional Proofs and the Deduction RulePhD thesis, U.C. Berkeley, 1991.

    Google Scholar 

  4. M. L. Bonet and S. R. BussSize-depth tradeoffs for Boolean formulasInformation Processing Letters, 29 (1994), pp. 151–155.

    MathSciNet  Google Scholar 

  5. M. L. Bonet, T. Pitassi, and R. RazLower bounds for cutting planes proofs with small coefficientsJournal of Symbolic Logic, 62 (1997), pp. 708–728. An earlier version appeared in Proc. Twenty-Seventh Annual ACM Symposium on the Theory of Computing 1995, pp. 575–584.

    Google Scholar 

  6. R. Boppana and M. SipserThe Complexity of Finite FunctionsMIT Press/Elsevier, 1990, pp. 757–804.

    Google Scholar 

  7. A. Borodin, S. Cook, and N. PippengerParallel computation for well-endowed rings and space-bounded probabilistic machinesInformation and Control, 58 (1992), pp. 113–136.

    MathSciNet  Google Scholar 

  8. R. P. BrentThe parallel evaluation of general arithmetic expressions, J. Assoc. Comput. Mach., 21(1974), pp. 201–206.

    Article  MathSciNet  MATH  Google Scholar 

  9. N. H. Bshouty, R. Cleve, and W. EberlySize-depth tradeoffs for algebraic formulaein Proceedings of the 32th Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society, 1991, pp. 334–341.

    Google Scholar 

  10. S. R. BussThe Boolean formula value problem is in ALOGTIMEin Proceedings of the 19-th Annual ACM Symposium on Theory of Computing, May 1987, pp. 123–131.

    Google Scholar 

  11. S. R. BussPolynomial size proofs of the propositional pigeonhole principleJournal of Symbolic Logic, 52 (1987), pp. 916–927.

    MathSciNet  MATH  Google Scholar 

  12. S. R. BussAn introduction to proof theory.Typeset manuscript, to appear in S.R. Buss (ed.) Handbook of Proof Theory, North-Holland, 199?

    Google Scholar 

  13. S. R. BussAlgorithms for Boolean formula evaluation and for tree con- traction, in Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Krajícek, eds., Oxford University Press, 1993, pp. 96–115.

    Google Scholar 

  14. S. R. BussSome remarks on lengths of propositional proofsArchive for Mathematical Logic, 34 (1995), pp. 377–394.

    Article  MathSciNet  MATH  Google Scholar 

  15. S. R. BussLectures in proof theoryTech. Rep. SOCS 96.1, School of Computer Science, McGill University, 1996. Notes from a series of lectures given at the at the McGill University Bellair’s Research Institute, Holetown, Barbados, March 1995. Scribe note written by E. Allender, M.L. Bonet, P. Clote, A. Maciel, P. McKenzie, T. Pitassi, R. Raz, K. Regan, J. Torán and C. Zamora.

    Google Scholar 

  16. S. R.. Buss and P. CloteCutting planes, connectivity and threshold logicArchive for Mathematical Logic, 35 (1996), pp. 33–62.

    MathSciNet  MATH  Google Scholar 

  17. S. R. Buss, S. A. Cook, A. Gupta, and V. RamachandranAn optimal parallel algorithm for formula evaluationSIAM J. Comput., 21 (1992), pp. 755–780.

    Article  MathSciNet  MATH  Google Scholar 

  18. V. Chvátal and E. SzemerédiMany hard examples for resolutionJournal of the ACM, 35 (1988), pp. 759–768.

    Article  MATH  Google Scholar 

  19. S. A. CookThe complexity of theorem proving techniquesin Proceedings of the 3-rd Annual ACM Symposium on Theory of Computing, 1971, pp. 151–158.

    Google Scholar 

  20. S. A. Cook and R. A. ReckhowThe relative efficiency of propositional proof systemsJournal of Symbolic Logic, 44 (1979), pp. 36–50.

    Article  MathSciNet  MATH  Google Scholar 

  21. W. Cook, C. R. Coullard, and G. TuránOn the complexity of cutting plane proofsDiscrete Applied Mathematics, 18 (1987), pp. 25–38.

    Article  MathSciNet  MATH  Google Scholar 

  22. W. CraigLinear reasoning. A new form of the Herbrand-Gentzen theoremJournal of Symbolic Logic, 22 (1957), pp. 250–268.

    Article  MathSciNet  MATH  Google Scholar 

  23. M. DowdModel-theoretic aspects of P≠ NP.Typewritten manuscript, 1985.

    Google Scholar 

  24. A. GoerdtCutting plane versus frege proof systemsin Computer Science Logic 1990, E. Börger, ed., Lecture Notes in Computer Science #552, 1992, pp. 174–194.

    Google Scholar 

  25. A. HakenThe intractability of resolutionTheoretical Computer Science, 39 (1985), pp. 297–308.

    Article  MathSciNet  MATH  Google Scholar 

  26. J. Hartmanis and R.. StearnsOn the computational complexity of algorithmsTransactions of the American Mathematical Society, 117 (1965), pp. 285–306.

    Article  MathSciNet  MATH  Google Scholar 

  27. S. Kosaraju and A. DelcherA tree-partitioning technique with applications to expression evaluation and term matchingin Proceedings of the Thirteenth Annual Symposium on Foundations of Computing, IEEE Computer Society, 1990, pp. 163–172.

    Google Scholar 

  28. J. KrajícekLower bounds to the size of constant-depth propositional proofsJournal of Symbolic Logic, 59 (1994), pp. 73–85.

    Article  MathSciNet  MATH  Google Scholar 

  29. J. KrajícekInterpolation theorems lower bounds for proof systems and independence results for bounded arithmeticJournal of Symbolic Logic, 62 (1997), pp. 457–486.

    Article  MathSciNet  MATH  Google Scholar 

  30. J. Krajíček and P. PudlákThe number of proof lines and the size of proofs in first-order logicArchive for Mathematical Logic, 27 (1988), pp. 69–84.

    Article  MathSciNet  MATH  Google Scholar 

  31. J. Krajícek and P. PudlakPropositional proof systems the consistency of first-order theories and the complexity of computationsJournal of Symbolic Logic, 54 (1989), pp. 1063–1079.

    Article  MathSciNet  MATH  Google Scholar 

  32. J. Krajícek, P. Pudlak, and A. WoodsExponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principleRandom Structures and Algorithms, 7 (1995), pp. 15–39.

    Article  MathSciNet  MATH  Google Scholar 

  33. R. E. LadnerThe circuitvalue problem is log space complete for P, SIGACT News, 7 (1975), pp. 18–20.

    Article  Google Scholar 

  34. D. MundiciTautologies with a unique Craig interpolantAnnals of Pure and Applied Logic, 27 (1984), pp. 265–273.

    Article  MathSciNet  MATH  Google Scholar 

  35. Y. OfmanOn the algorithmic complexity of discete functionsDoklady Akad. Nauk SSSR, 145 (1962), pp. 48–51. English translation in Soviet Physics - Doklady 7 (1963)589–591.

    Google Scholar 

  36. T. Pitassi, P. Beame, and R. ImpagliazzoExponential lower bounds for the pigeonhole principleComputational Complexity, 3 (1993), pp. 97–140.

    Article  MathSciNet  MATH  Google Scholar 

  37. P. PudlakLower bounds for resolution and cutting planes proofs and monotone computationsJournal of Symbolic Logic, 62 (1997), pp. 981–998.

    Article  MathSciNet  MATH  Google Scholar 

  38. A. A. RazborovLower bounds on the monotone complexity of some Boolean functionsSoviet Mathematics Doklady, 31 (1985), pp. 354–357.

    MATH  Google Scholar 

  39. R. A. ReckhowOn the Lengths of Proofs in the Propositional CalculusPhD thesis, Department of Computer Science, University of Toronto, 1976. Technical Report #87.

    Google Scholar 

  40. J. Siekmann and G. WrightsonAutomation of Reasoningvol. 1&2, Springer-Verlag, Berlin, 1983.

    Book  Google Scholar 

  41. P. M. SpiraOn time hardware complexity tradeoffs for Boolean functionsin Proceedings of the Fourth Hawaii International Symposium on System Sciences, 1971, pp. 525–527.

    Google Scholar 

  42. R. StatmanComplexity of derivations from quantifier-free Horn formulae,mechanical introduction of explicit definitions and refinent of completeness theorems, in Logic Colloquium ‘76, R. Gandy and M.Hyland, eds., Amsterdam, 1977, North-Holland, pp. 505–517.

    MATH  Google Scholar 

  43. G. S. TsejtinOn the complexity of derivation in propositional logicStudies in Constructive Mathematics and Mathematical Logic, 2 (1968), pp. 115–125. Reprinted in: [40, vol 2].

    Google Scholar 

  44. C. S. WallaceA suggestions for a fast multiplierIEEE Transactions on Computers, EC-13 (1964), pp. 14–17.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departments of Mathematics and Computer Science, University of California, San Diego, USA

    Samuel R. Buss

Authors
  1. Samuel R. Buss
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematics, University of Munich, Theresienstr. 39, Munich, D-80333, Germany

    Ulrich Berger  & Helmut Schwichtenberg  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Buss, S.R. (1999). Propositional Proof Complexity an Introduction. In: Berger, U., Schwichtenberg, H. (eds) Computational Logic. NATO ASI Series, vol 165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-58622-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-58622-4_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-63670-7

  • Online ISBN: 978-3-642-58622-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation