Skip to main content
SpringerLink
Log in

On Methods for Proving Lower Bounds in Propositional Logic

  • Chapter
Logic and Scientific Methods

Part of the book series: Synthese Library ((SYLI,volume 259))

Abstract

This paper is based on my lecture [26]. It examines the problem of proving non-trivial lower bounds for the length of proofs in propositional logic from the perspective of methods available rather than surveying known partial results (i.e., lower bounds for weaker proof systems). We discuss neither motivations for proving lower bounds for propositional logic nor relations to other problems in logic or complexity theory. The reader is referred to [20] for the background information (as well as for all details missing in this paper). The paper is aimed at curious non-specialists. The style of our exposition is accordingly informal at places. and we do not burden the text (especially in the introduction) with exhausting references not directly related to our main objective. The reader starving for details can find them, together with all original references, in [20] (see also expository articles [25, 32]) .

Partially supported by the US — Czechoslovak Science and Technology Program grant # 93025, and by the grant #119107 of the AV ČR.

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

Access this chapter

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 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Ajtai: The complexity of the pigeonhole principle, in: Proc. IEEE 29th Annual Symp. on Foundation of Computer Science, (1988), pp. 346–355.

    Google Scholar 

  2. A. E. Andreev: On a method for obtaining lower bounds for the complexity of individual monotone functions (in Russian), Doklady AN SSSR, 282(5), (1985), pp.1033–1037.

    Google Scholar 

  3. Current issues in quantum logic, Eds. E.G.Beltrametti and B.van Fraassen, Plenum Press, New York-London, Ettore Majorana International Science Series, Vol.8, Proc. of the Workshop on Quantum Logic held Dec.2–9, 1979 in Erice, Sicily. (1981) .

    Google Scholar 

  4. P. Beame, R. Impagliazzo, J. Krajíček, T. Pitassi and P.Pudlák: Lower bounds on Hilbert’s Nullstellensatz and propositional proofs, Proceedings of the London Mathematical Society, to appear.

    Google Scholar 

  5. G. Birkhoff and J. von Neumann: The logic of quantum mechanics, Annals of Mathematics, 37, (1936), pp.823–843. Reprinted in The logico-algebraic approach to quantum mechanics, Vol.I., Ed. C.A.Hooker, D.Reidel Publ.Co., Dordrecht-Boston, (1975).

    Article  Google Scholar 

  6. M. L. Bonet, T. Pitassi, and R. Raz: Lower bounds for cutting planes proofs with small coefficients, preprint, (1994).

    Google Scholar 

  7. S. Buss: Thé propositional pigeonhole principle has polynomial size Frege proofs, J. Symbolic Logic 52, (1987), pp. 916–927.

    Article  Google Scholar 

  8. S. Buss and P. Pudlák: How to lie without being (easily) convicted and the length of proofs in propositional calculus, in: Proceedings of the meeting Computer Science Logic, Kazimierz 1994, Eds. L.Pacholski and J.Tiuryn, LNCS 933, Springer-Verlag, (1995), pp.151–162.

    Google Scholar 

  9. S.A. Cook and A.R. Reckhow: The relative efficiency of propositional proof systems, J. Symbolic Logic, 44(1), (1979), pp. 36–50.

    Article  Google Scholar 

  10. T. Evans: Word problems, Bulletin of the AMS, 84(5), (1978), pp.789–802.

    Article  Google Scholar 

  11. G. Gratzer: Universal algebra (2nd ed.), Springer — Verlag, (1979), 581 p.

    Google Scholar 

  12. A. Haken: The intractability of resolution, Theoretical Computer Science, 39, (1985), pp. 297–308.

    Article  Google Scholar 

  13. A. Haken: Counting bottlenecks to show monotone P ≠ NP, in: Proc. IEEE 36th Annual Symp. of Foundations of Computer Science, (1995), pp. 36–40.

    Google Scholar 

  14. E.V. Huntington: Sets of independent postulates for the algebra of logic, Transaction of the AMS, 5, (1904), pp.288–309.

    Article  Google Scholar 

  15. J.M. Jauch: Foundations of quantum mechanics, Addison-Wesley, Reading-Menlo Park-London-Don Mills, Series in Advanced Physics, (1968).

    Google Scholar 

  16. M. Karchmer: On proving lower bounds for circuit size, in: Proc. Structure in Complexity, 8th Annual Conference, IEEE Computer Science Press, (1993), pp. 112–119.

    Google Scholar 

  17. S. Kochen and E. Specker: Logical structures arising in quantum theory, in: The theory of models, Eds. J. Addison, L. Henkin and A. Tarski, North-Holland, Amsterdam, (1956). Reprinted in The logico-algebraic approach to quantum mechanics, Vol.I., Ed. C.A.Hooker, D.Reidel Publ.Co., Dordrecht-Boston, (1975).

    Google Scholar 

  18. S. Kochen and E. Specker: The calculus of partial propositional functions, in: Logic, Methodology and Philosophy Science, Ed. Y. Bar-Hillel, North-Holland, Amsterdam, (1965). Reprinted in The logico-algebraic approach to quantum mechanics, Vol.I., Ed. C.A.Hooker, D.Reidel Publ.Co., Dordrecht-Boston, (1975).

    Google Scholar 

  19. S. Kochen and E. Specker: The problem of hidden variables in quantum mechanics, J. of Mathematics and Mechanics, 17, (1967), pp.59–67. Reprinted in The logico-algebraic approach to quantum mechanics, Vol.I., Ed. C.A.Hooker, D.Reidel Publ.Co., Dordrecht-Boston, (1975).

    Google Scholar 

  20. J. Krajíček: Bounded arithmetic, propositional logic and complexity theory, Cambridge University Press, Cambridge-New York-Melbourne, (1995).

    Book  Google Scholar 

  21. S. Kochen and E. Specker: Speed-up for propositional Frege systems via generalizations of proofs, Commentationes Mathematicae Universitas Carolinae, 30(1), (1989), pp.137–140.

    Google Scholar 

  22. S. Kochen and E. Specker: Lower bounds to the size of constant-depth propositional proofs, J. of Symbolic Logic, 59(1), (1994), pp.73–86.

    Article  Google Scholar 

  23. S. Kochen and E. Specker: On Frege and extended Frege proof systems, in: Feasible Mathematics II, Eds. P. Clote and J. Remmel, Birkhauser, (1995), pp. 284–319.

    Google Scholar 

  24. S. Kochen and E. Specker: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. of Symbolic Logic, (1995), to appear.

    Google Scholar 

  25. S. Kochen and E. Specker: A fundamental problem of mathematical logic, Annals of Kurt Gödel Society, Springer Verlag, (1995), to appear.

    Google Scholar 

  26. S. Kochen and E. Specker: Valuations of Boolean formulae in partial algebras, in: Volume of Abstracts of the Tenth International Congress Logic, Methodology and Philosophy of Science, International Union of History and Philosophy of Science, Florence (August 19–25, 1995), (1995), pp.6–7.

    Google Scholar 

  27. J. Krajíček and P. Pudlák: Some consequences of cryptographical conjectures for S1 2 and EF, Proc. of the meeting Logic and Computational Complexity, (Indianapolis, October 1994), Ed. D. Leivant, Lecture Notes in Computer Science, Vol. 960, Springer-Verlag, (1995), pp. 210–220.

    Google Scholar 

  28. J. Krajíček, P. Pudlák and A. Woods: An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures and Algorithms, 7(1), (1995), pp.15–39.

    Article  Google Scholar 

  29. A. Lewenberg: On elementary pairs of O-minimal structures, PhD.Thesis, University of Illinois at Champaign-Urbana, (1995) .

    Google Scholar 

  30. P. Mittelstaedt: Quantum logic, D. Reidel Publ.Co., Dordrecht, Synthese Library, Vol. 126, (1978).

    Book  Google Scholar 

  31. T. Pitassi, P. Beame and R. Impagliazzo: Exponential lower bounds for the pigeonhole principle, Computational Complexity, 3, (1993), pp.97–308.

    Article  Google Scholar 

  32. P. Pudlák: The lengths of proofs, in: Handbook of Proof Theory, Ed. S. Buss, to appear.

    Google Scholar 

  33. P. Pudlák: Lower bounds for resolution and cutting planes proofs and monotone computations, preprint, (1995).

    Google Scholar 

  34. A. A. Razborov: Lower bounds on the monotone complexity of some Boolean functions, Soviet Mathem. Doklady, 31, (1985), pp.354–357.

    Google Scholar 

  35. A. A. Razborov: Lower bounds on the size of bounded depth networks over a complete basis with logical addition, Matem. Zametki, 41(4), (1987), pp.598–607.

    Google Scholar 

  36. A. A. Razborov: On the method of approximations, in: Proc. 21th Annual ACM Symp. on Theory of Computing, (1989), pp. 168–176. ACM Press.

    Google Scholar 

  37. A. A. Razborov: Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic, Izvestiya of the R.A.N., 59(1), (1995), pp.201–224.

    Google Scholar 

  38. R. Smolensky: Algebraic methods in the theory of lower bounds for Boolean circuit complexity, in: Proc. 19th Ann. ACM Symp. on Th. of Computing, (1987), pp. 77–82.

    Google Scholar 

  39. E. P. Specker: The logic of propositions which are not simultaneously decidable, Dialectica, 14, (1960), pp.239–246. Reprinted in The logico-algebraic approach to quantum mechanics, Vol.I., Ed. C.A.Hooker, D.Reidel Publ.Co., Dordrecht-Boston, (1975).

    Article  Google Scholar 

  40. E.-W. Stachow: Completeness of quantum logic, J. Phil. Logic, 5, (1976), pp.237–280.

    Article  Google Scholar 

  41. G. Takeuti: Quantum set theory, in: [3], pp.303–322.

    Google Scholar 

  42. G. Takeuti: Quantum logic and quantization, in; Proc. Int. Symp. Foundations of Quantum Mechanics, Tokyo, (1983), pp.256–260.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematical Institute of the Academy of Sciences, Prague, Czech Republic

    Jan Krajíček

Authors
  1. Jan Krajíček
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Florence, Italy

    Maria Luisa Dalla Chiara

  2. University of Amsterdam, The Netherlands

    Kees Doets  & Johan van Benthem  & 

  3. University of Milan, Italy

    Daniele Mundici

  4. Stanford University, USA

    Johan van Benthem

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Krajíček, J. (1997). On Methods for Proving Lower Bounds in Propositional Logic. In: Dalla Chiara, M.L., Doets, K., Mundici, D., van Benthem, J. (eds) Logic and Scientific Methods. Synthese Library, vol 259. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0487-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-0487-8_4

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-4786-1

  • Online ISBN: 978-94-017-0487-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation