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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Ajtai, M.: The complexity of the pigeonhole principle. In: Proc. IEEE 29th Annual Symp. on Foundation of Computer Science, pp. 346–355 (1988)
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)
Beame, P.: A switching lemma primer. Technical Report UW-CSE-95-07-01, Department of Computer Science and Engineering, University of Washington (November 1994)
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)
Bonet, M., Pitassi, T., Raz, R.: No feasible interpolation for TC 0-Frege proofs. In: Proc. 38-th FOCS, pp. 254–263 (1997)
Buss, S.R.: Bounded Arithmetic. Bibliopolis (1986)
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)
Buss, S., Pudlák, P.: On the computational content of intuitionistic propositional proofs. Annals of Pure and Applied Logic 109, 49–64 (2001)
Chattopadhyay, A., Ada, A.: Multiparty Communication Complexity of Disjointness. arXiv e-print (arXiv:0801.3624)
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)
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)
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. Journ. Symbolic Logic 44, 25–38 (1987)
Dalla Chiara, M.L., Giuntini, R.: Quantum Logics. In: Gabbay, Guenthner (eds.) Handbook of Philosophical Logic, pp. 129–228. Kluwer Academic Publishers, Dordrecht (2002)
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)
Egly, U., Tompits, H.: On different proof-search strategies for orthologic. Stud. Log. 73, 131–152 (2003)
Hrubeš, P.: A lower bound for intuitionistic logic. Ann. Pure Appl. Logic 146(1), 72–90 (2007)
Hrubeš, P.: Lower bounds for modal logics. Journ. Symbolic Logic (to appear)
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)
Krajíček, J.: Lower Bounds to the Size of Constant-Depth Propositional Proofs. J. of Symbolic Logic 59(1), 73–86 (1994)
Krajıček, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. In: Encyclopedia of Mathematics and its Applications 60, Cambridge Univ. Press, Cambridge (1995)
Krajíček, J.: A fundamental problem of mathematical logic. Collegium Logicum, Annals of Kurt Gödel Society 2, 56–64 (1996)
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)
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
Krajíček, J.: On the weak pigeonhole principle. Fundamenta Mathematicae 170(1-3), 123–140 (2001)
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)
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)
Krajíček, J., Pudlák, P., Takeuti, G.: Bounded Arithmetic and the Polynomial Hierarchy. Annals of Pure and Applied Logic 52, 143–153 (1991)
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)
Krajíček, J., Pudlák, P.: Some consequences of cryptographical conjectures for \(S^1_2\) and EF. Information and Computation 140, 82–94 (1998)
Krajíček, J., Impagliazzo, R.: A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly 48(3), 375–377 (2002)
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)
Lee, T., Schraibman, A.: Disjointness is hard in the multi-party number on the forehead model. arXiv e-print (arXiv:0712.4279)
Lovász, L., Schrijver, A.: Cones of matrices and set-functions and 0-1 optimization. SIAM J. Optimization 1(2), 166–190 (1991)
Pitassi, T., Beame, P., Impagliazzo, R.: Exponential Lower Bounds for the Pigeonhole Principle. Computational Complexity 3, 97–140 (1993)
Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symbolic Logic 62(3), 981–998 (1997)
Pudlák, P.: The lengths of proofs. In: Handbook of Proof Theory, pp. 547–637. Elsevier, Amsterdam (1998)
Pudlák, P.: On reducibility and symmetry of disjoint NP-pairs. Theor. Comput. Science 295, 323–339 (2003)
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)
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
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)
Razborov, A.A.: On provably disjoint NP-pairs. BRICS Report Series RS-94-36 (1994), http://www.brics.dk/RS/94/36/index.html
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
Razborov, A.A.: Bounded Arithmetic and Lower Bounds in Boolean Complexity. In: Feasible Mathematics II, pp. 344–386. Birkhäuser Verlag (1995)
Razborov, A.A.: Lower bound for the polynomial calculus. Computational Complexity 7(4), 291–324 (1998)
Razborov, A.A.: Pseudorandom Generators Hard for k-DNF Resolution and Polynomial Calculus Resolution (2002-2003), http://www.mi.ras.ru/~razborov/resk.ps
Skelley, A., Thapen, N.: The provably total search problems of Bounded Arithmetic (preprint, 2007)
Smolensky, R.: Algebraic Methods in the Theory of Lower Bounds for Boolean Circuit Complexity. In: STOC, pp. 77–82 (1987)
Author information
Authors and Affiliations
Editor information
Rights 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)