Skip to main content
SpringerLink
Log in

Twelve Problems in Proof Complexity

  • Conference paper
Computer Science – Theory and Applications (CSR 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5010))

Included in the following conference series:

Abstract

Proof complexity is a research area that studies the concept of complexity from the point of view of logic. Although it is very much connected with computational complexity, the goals are different. In proof complexity we are studying the question how difficult is to prove a theorem? There are various ways how one can measure the “complexity” of a theorem. We may ask what is the length of the shortest proof of the theorem in a given formal system. Thus the complexity is the size of proofs. This corresponds to questions in computational complexity about the size of circuits, the number of steps of Turing machines etc. needed to compute a given function. But we may also ask how strong theory is needed to prove the theorem. This also has a counterpart in computational complexity—the questions about the smallest complexity class to which a given set or function belongs.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Google Scholar 

  2. Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Pseudorandom Generators in Propositional Proof Complexity. SIAM Journal on Computing 34(1), 67–88 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  3. Beame, P.: A switching lemma primer. Technical Report UW-CSE-95-07-01, Department of Computer Science and Engineering, University of Washington (November 1994)

    Google Scholar 

  4. Beame, P., Pitassi, T., Segerlind, N.: Lower Bounds for Lovász-Schrijver Systems and Beyond Follow from Multiparty Communication Complexity. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1176–1188. Springer, Heidelberg (2005)

    Google Scholar 

  5. Bonet, M., Pitassi, T., Raz, R.: No feasible interpolation for TC 0-Frege proofs. In: Proc. 38-th FOCS, pp. 254–263 (1997)

    Google Scholar 

  6. Buss, S.R.: Bounded Arithmetic. Bibliopolis (1986)

    Google Scholar 

  7. Buss, S., Impagliazzo, R., Krajíček, J., Pudlák, P., Razborov, A.A., Sgall, J.: Proof complexity in algebraic systems and constant depth Frege systems with modular counting. Computational Complexity 6, 256–298 (1996(/1997)

    Google Scholar 

  8. Buss, S., Pudlák, P.: On the computational content of intuitionistic propositional proofs. Annals of Pure and Applied Logic 109, 49–64 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  9. Chattopadhyay, A., Ada, A.: Multiparty Communication Complexity of Disjointness. arXiv e-print (arXiv:0801.3624)

    Google Scholar 

  10. Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proc. 28-th ACM STOC, pp. 174–183 (1996)

    Google Scholar 

  11. Clote, P., Krajíček, J.: Open Problems. In: Clote, P., Krajíček, J. (eds.) Arithmetic, Proof Theory and Computational Complexity, pp. 1–19. Oxford Press (1993)

    Google Scholar 

  12. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. Journ. Symbolic Logic 44, 25–38 (1987)

    MathSciNet  Google Scholar 

  13. Dalla Chiara, M.L., Giuntini, R.: Quantum Logics. In: Gabbay, Guenthner (eds.) Handbook of Philosophical Logic, pp. 129–228. Kluwer Academic Publishers, Dordrecht (2002)

    Google Scholar 

  14. Dash, S.: An Exponential Lower Bound on the Length of Some Classes of Branch-and-Cut Proofs. In: Cook, W.J., Schulz, A.S. (eds.) IPCO 2002. LNCS, vol. 2337, pp. 145–160. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Egly, U., Tompits, H.: On different proof-search strategies for orthologic. Stud. Log. 73, 131–152 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hrubeš, P.: A lower bound for intuitionistic logic. Ann. Pure Appl. Logic 146(1), 72–90 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  17. Hrubeš, P.: Lower bounds for modal logics. Journ. Symbolic Logic (to appear)

    Google Scholar 

  18. Kojevnikov, A., Itsykson, D.: Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4051, pp. 323–334. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Krajíček, J.: Lower Bounds to the Size of Constant-Depth Propositional Proofs. J. of Symbolic Logic 59(1), 73–86 (1994)

    Article  MATH  Google Scholar 

  20. Krajıček, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. In: Encyclopedia of Mathematics and its Applications 60, Cambridge Univ. Press, Cambridge (1995)

    Google Scholar 

  21. Krajíček, J.: A fundamental problem of mathematical logic. Collegium Logicum, Annals of Kurt Gödel Society 2, 56–64 (1996)

    Google Scholar 

  22. Krajıček, J.: Lower bounds for a proof system with an exponential speed-up over constant-depth Frege systems and over polynomial calculus. In: Privara, I., Ružička, P. (eds.) MFCS 1997. LNCS, vol. 1295, pp. 85–90. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  23. Krajíček, J.: On methods for proving lower bounds in propositional logic. In: Dalla Chiara, M.L., et al. (eds.) Logic and Scientific Methods, pp. 69–83. Kluwer Acad. Publ., Dordrecht

    Google Scholar 

  24. Krajíček, J.: On the weak pigeonhole principle. Fundamenta Mathematicae 170(1-3), 123–140 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  25. Krajíček, J.: Proof complexity. In: Laptev, A. (ed.) European congress of mathematics (ECM), Stockholm, Sweden, June 27–July 2, 2004, pp. 221–231. European Mathematical Society (2005)

    Google Scholar 

  26. Krajíček, J.: A proof complexity generator. In: Glymour, C., Wang, W., Westerstahl, D. (eds.) Proc. 13th Int. Congress of Logic, Methodology and Philosophy of Science, Beijing. ser. Studies in Logic and the Foundations of Mathematics. King’s College Publications, London (to appear, 2007)

    Google Scholar 

  27. Krajíček, J., Pudlák, P., Takeuti, G.: Bounded Arithmetic and the Polynomial Hierarchy. Annals of Pure and Applied Logic 52, 143–153 (1991)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  29. Krajíček, J., Pudlák, P.: Some consequences of cryptographical conjectures for \(S^1_2\) and EF. Information and Computation 140, 82–94 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  30. Krajíček, J., Impagliazzo, R.: A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly 48(3), 375–377 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  31. Krajíček, J., Skelley, A., Thapen, N.: NP search problems in low fragments of bounded arithmetic. J. of Symbolic Logic 72(2), 649–672 (2007)

    Article  MATH  Google Scholar 

  32. Lee, T., Schraibman, A.: Disjointness is hard in the multi-party number on the forehead model. arXiv e-print (arXiv:0712.4279)

    Google Scholar 

  33. Lovász, L., Schrijver, A.: Cones of matrices and set-functions and 0-1 optimization. SIAM J. Optimization 1(2), 166–190 (1991)

    Article  MATH  Google Scholar 

  34. Pitassi, T., Beame, P., Impagliazzo, R.: Exponential Lower Bounds for the Pigeonhole Principle. Computational Complexity 3, 97–140 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  35. Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symbolic Logic 62(3), 981–998 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  36. Pudlák, P.: The lengths of proofs. In: Handbook of Proof Theory, pp. 547–637. Elsevier, Amsterdam (1998)

    Chapter  Google Scholar 

  37. Pudlák, P.: On reducibility and symmetry of disjoint NP-pairs. Theor. Comput. Science 295, 323–339 (2003)

    Article  MATH  Google Scholar 

  38. Pudlák, P.: Consistency and games—in search of new combinatorial principles. In: Helsinki, Stoltenberg-Hansen, V., Vaananen, J. (eds.) Proc. Logic Colloquium 2003. Assoc. for Symbolic Logic, pp. 244–281 (2006)

    Google Scholar 

  39. Pudlák, P., Sgall, J.: Algebraic models of computation and interpolation for algebraic proof systems. In: Beame, P.W., Buss, S.R. (eds.) Proof Complexity and Feasible Arithmetics. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 39, pp. 279–295

    Google Scholar 

  40. Razborov, A.A.: Lower bounds on the size of bounded-depth networks over a complete basis with logical addition (Russian). Matematicheskie Zametki 41(4), 598–607 (1987); English translation in: Mathematical Notes of the Academy of Sci. of the USSR 41(4), 333–338 (1987)

    Google Scholar 

  41. Razborov, A.A.: On provably disjoint NP-pairs. BRICS Report Series RS-94-36 (1994), http://www.brics.dk/RS/94/36/index.html

  42. Razborov, A.A.: Unprovability of lower bounds on the circuit size in certain fragments of Bounded Arithmetic. Izvestiya of the R.A.N. 59(1), 201–222 (1995); see also Izvestiya: Mathematics 59(1), 205–227

    Google Scholar 

  43. Razborov, A.A.: Bounded Arithmetic and Lower Bounds in Boolean Complexity. In: Feasible Mathematics II, pp. 344–386. Birkhäuser Verlag (1995)

    Google Scholar 

  44. Razborov, A.A.: Lower bound for the polynomial calculus. Computational Complexity 7(4), 291–324 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  45. Razborov, A.A.: Pseudorandom Generators Hard for k-DNF Resolution and Polynomial Calculus Resolution (2002-2003), http://www.mi.ras.ru/~razborov/resk.ps

  46. Skelley, A., Thapen, N.: The provably total search problems of Bounded Arithmetic (preprint, 2007)

    Google Scholar 

  47. Smolensky, R.: Algebraic Methods in the Theory of Lower Bounds for Boolean Circuit Complexity. In: STOC, pp. 77–82 (1987)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematical Institute, Prague

    Pavel Pudlák

Authors
  1. Pavel Pudlák
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Edward A. Hirsch Alexander A. Razborov Alexei Semenov Anatol Slissenko

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pudlák, P. (2008). Twelve Problems in Proof Complexity. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds) Computer Science – Theory and Applications. CSR 2008. Lecture Notes in Computer Science, vol 5010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79709-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-79709-8_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-79708-1

  • Online ISBN: 978-3-540-79709-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation