Skip to main content
SpringerLink
Log in
Book cover

Logic from Computer Science pp 597–608Cite as

Complexity of Proofs in Classical Propositional Logic

  • Conference paper

Part of the book series: Mathematical Sciences Research Institute Publications ((MSRI,volume 21))

Abstract

This paper surveys the work of the last two decades on the complexity of proofs in classical propositional logic, and its connection with open problems in theoretical computer science. The paper ends with a short list of open problems.

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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight 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. Miklos Ajtai ‘The complexity of the pigeonhole principle’, forthcoming. Preliminary version, 29th Annual Symposium on the Foundations of Computer Science (1988), 346–55.

    Google Scholar 

  2. Samuel R . Buss. Bounded Arithmetic. Ph.D. dissertation, Princeton University 1985; revised version Bibliopolis Naples, 1986.

    Google Scholar 

  3. Samuel R. Buss. ‘Polynomial size proofs of the propositional pigeonhole principle’, J. Symbolic Logic, Vol. 52 (1987), 916–27.

    Article  MathSciNet  MATH  Google Scholar 

  4. Samuel R. Buss and György Turän. ‘Resolution proofs of generalized pigeonhole principles’, Theoretical Computer Science, Vol. 62 (1988), 311–17.

    Article  MathSciNet  MATH  Google Scholar 

  5. Stephen A. Cook. ‘Feasibly constructive proofs and the propositional calculus’, Proc. 7th A.CM. Symposium on the Theory of Computation, 83–97.

    Google Scholar 

  6. Stephen A. Cook and Robert A. Reckhow. ‘The relative efficiency of propositional proof systems’, J. Symbolic Logic Vol. 44 (1979), 36–50.

    Article  MathSciNet  Google Scholar 

  7. Martin Dowd. Propositional representation of arithmetic proofs. Ph.D. dissertation, University of Toronto, 1979.

    Google Scholar 

  8. Martin Dowd. ‘Model-theoretic aspects of P ≠ NP’, preprint, 1985.

    Google Scholar 

  9. Paul E. Dunne. The Complexity of Boolean Networks. Academic Press, London and San Diego, 1988.

    MATH  Google Scholar 

  10. Martin Gardner. Logic machines, diagrams and Boolean algebra. Dover Publications, Inc. New York 1968.

    Google Scholar 

  11. Armin Haken ‘The intractability of resolution’, Theoretical Computer Science, Vol. 39 (1985), 297–308.

    Article  MathSciNet  MATH  Google Scholar 

  12. Johan T. Håstad. Computational limitations of small-depth circuits. The MIT Press, Cambridge, Massachusetts, 1987.

    Google Scholar 

  13. Jan Krajíček and Pavel Pudlák. ‘Propositional proof systems, the consistency of first order theories and the complexity of computations’, J. Symbolic Logic, Vol. 54 (1989), 1063–79.

    Article  MathSciNet  MATH  Google Scholar 

  14. Jan Krajíček and Pavel Pudlák. ‘Quantified propositional calculi and fragments of bounded arithmetic’, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik (to appear).

    Google Scholar 

  15. W.V. Quine. ‘Two theorems about truth functions’, Bol. Soc. Math. Mex. Vol. 10, 64–70.

    Google Scholar 

  16. W.V. Quine. ‘A way to simplify truth functions’, Am. Math. Monthly Vol. 62 (1955), 627–631.

    Article  MathSciNet  Google Scholar 

  17. Robert A. Reckhow On the lengths of proofs in the propositional calculus. Ph.D. thesis, Department of Computer Science, University of Toronto, 1976.

    Google Scholar 

  18. Jörg Siekmann and Graham Wrightson (eds.) Automation of Reasoning. Springer-Verlag, New York, 1983.

    Google Scholar 

  19. Richard Statman ‘Bounds for proof-search and speed-up in the predicate calculus’, Annals of mathematical logic Vol. 15, 225–87.

    Google Scholar 

  20. G.S. Tseitin ‘On the complexity of derivation in propositional calculus’, Studies in Constructive Mathematics and Mathematical Logic Part 2. Seminars in mathematics, V.A. Steklov Math. Institute 1968. Reprinted in [18].

    Google Scholar 

  21. Alasdair Urquhart ‘The complexity of Gentzen systems for propositional logic’, Theoretical Computer Science Vol. 66 (1989), 87–97.

    Article  MathSciNet  Google Scholar 

  22. Alasdair Urquhart ‘The relative complexity of resolution and cut-free Gentzen systems’, forthcoming, Discrete Applied Mathematics.

    Google Scholar 

  23. Hao Wang. ‘Towards mechanical mathematics’, IBM Journal for Research and Development Vol. 4 (1960), 2–22. Reprinted in [18].

    Article  Google Scholar 

  24. Ludwig Wittgenstein. Tractatus Logico-Philosophicus. Kegan Paul Ltd, London 1922.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departmnet of Philosophy, University of Toronto, Canada

    Alasdair Urquhart

Authors
  1. Alasdair Urquhart
    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 California at Los Angeles, 90024-1766, Los Angeles, CA, USA

    Yiannis N. Moschovakis

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag New York, Inc

About this paper

Cite this paper

Urquhart, A. (1992). Complexity of Proofs in Classical Propositional Logic. In: Moschovakis, Y.N. (eds) Logic from Computer Science. Mathematical Sciences Research Institute Publications, vol 21. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-2822-6_22

Download citation

  • DOI: https://doi.org/10.1007/978-1-4612-2822-6_22

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4612-7685-2

  • Online ISBN: 978-1-4612-2822-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation