Remote Access Proceedings of the American Mathematical Society
Green Open Access

Proceedings of the American Mathematical Society

ISSN 1088-6826(online) ISSN 0002-9939(print)

Request Permissions   Purchase Content 


A reduction of proof complexity to computational complexity for $ AC^0[p]$ Frege systems

Author: Jan Krajíček
Journal: Proc. Amer. Math. Soc. 143 (2015), 4951-4965
MSC (2010): Primary 03F20, 68Q17
Published electronically: April 2, 2015
MathSciNet review: 3391052
Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: We give a general reduction of lengths-of-proofs lower bounds for constant depth Frege systems in DeMorgan language augmented by a connective counting modulo a prime $ p$ (the so-called $ AC^0[p]$ Frege systems) to computational complexity lower bounds for search tasks involving search trees branching upon values of maps on the vector space of low degree polynomials over $ {{\bf F}_p}$.

References [Enhancements On Off] (What's this?)

  • [1] Miklos Ajtai, $ \Sigma ^{1}_{1}$-formulae on finite structures, Ann. Pure Appl. Logic 24 (1983), no. 1, 1-48. MR 706289 (85b:03048),
  • [2] Miklos Ajtai, The complexity of the pigeonhole principle, in: Proc. IEEE 29 $ ^{\mbox {th}}$ Annual Symp. on Foundation of Computer Science, (1988), pp. 346-355.
  • [3] Miklos Ajtai, Parity and the pigeonhole principle, Feasible mathematics (Ithaca, NY, 1989) Progr. Comput. Sci. Appl. Logic, vol. 9, Birkhäuser Boston, Boston, MA, 1990, pp. 1-24. MR 1232921 (94g:03112)
  • [4] Miklos Ajtai, The independence of the modulo $ p$ counting principles, in: Proceedings of the 26th Annual ACM Symposium on Theory of Computing, (1994), pp.402-411. ACM Press.
  • [5] Miklos Ajtai, Symmetric Systems of Linear Equations modulo p, in: Electronic Colloquium on Computational Complexity (ECCC), TR94-015, (1994).
  • [6] Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák, Lower bounds on Hilbert's Nullstellensatz and propositional proofs, Proc. London Math. Soc. (3) 73 (1996), no. 1, 1-26. MR 1387081 (97e:03072),
  • [7] Toniann Pitassi, Paul Beame, and Russell Impagliazzo, Exponential lower bounds for the pigeonhole principle, Comput. Complexity 3 (1993), no. 2, 97-140. MR 1233662 (94f:03019),
  • [8] Samuel R. Buss, Lower bounds on Nullstellensatz proofs via designs, Proof complexity and feasible arithmetics (Rutgers, NJ, 1996) DIMACS Ser. Discrete Math. Theoret. Comput. Sci., vol. 39, Amer. Math. Soc., Providence, RI, 1998, pp. 59-71. MR 1486614 (99c:03083)
  • [9] Samuel Buss, R. Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Comput. Complexity 6 (1996/97), no. 3, 256-298. MR 1486929 (99g:03060),
  • [10] Samuel R. Buss, Leszek A. Kolodziejczyk, and Konrad Zdanowski: Collapsing modular counting in bounded arithmetic and constant depth propositional proofs, Trans. Amer. Math. Soc, to appear.
  • [11] Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, Proceedings of the Twenty-eighth Annual ACM Symposium on the Theory of Computing (Philadelphia, PA, 1996) ACM, New York, 1996, pp. 174-183. MR 1427512,
  • [12] Stephen A. Cook and Robert A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44 (1979), no. 1, 36-50. MR 523487 (80e:03007),
  • [13] Merrick Furst, James B. Saxe, and Michael Sipser, Parity, circuits, and the polynomial-time hierarchy, Math. Systems Theory 17 (1984), no. 1, 13-27. MR 738749 (86e:68048),
  • [14] Johan Hastad, Almost optimal lower bounds for small depth circuits. in: Randomness and Computation, ed. S.Micali, Ser.Adv.Comp.Res., 5, (1989), pp.143-170. JAI Pres.
  • [15] Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall, Lower bounds for the polynomial calculus and the Gröbner basis algorithm, Comput. Complexity 8 (1999), no. 2, 127-144. MR 1724604 (2001g:68104),
  • [16] Russell Impagliazzo and Nathan Segerlind, Counting axioms do not polynomially simulate counting gates (extended abstract), 42nd IEEE Symposium on Foundations of Computer Science (Las Vegas, NV, 2001), IEEE Computer Soc., Los Alamitos, CA, 2001, pp. 200-209. MR 1948708
  • [17] Jan Krajíček, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic 59 (1994), no. 1, 73-86. MR 1264964 (95k:03093),
  • [18] Jan Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and its Applications, vol. 60, Cambridge University Press, Cambridge, 1995. MR 1366417 (97c:03003)
  • [19] Jan Krajíček, Lower bounds for a proof system with an exponential speed-up over constant-depth Frege systems and over polynomial calculus, Mathematical foundations of computer science 1997 (Bratislava), Lecture Notes in Comput. Sci., vol. 1295, Springer, Berlin, 1997, pp. 85-90. MR 1640210 (99e:03038),
  • [20] Jan Krajíček, On the degree of ideal membership proofs from uniform families of polynomials over a finite field, Illinois J. Math. 45 (2001), no. 1, 41-73. MR 1849985 (2003e:03113)
  • [21] Jan Krajíček, Forcing with random variables and proof complexity, London Mathematical Society Lecture Note Series, vol. 382, Cambridge University Press, Cambridge, 2011. MR 2768875 (2012h:03003)
  • [22] Jan Krajíček, Pavel Pudlák, and Alan Woods, An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures Algorithms 7 (1995), no. 1, 15-39. MR 1346282 (96i:03053),
  • [23] Alexis Maciel and Toniann Pitassi, Towards lower bounds for bounded-depth Frege proofs with modular connectives, Proof complexity and feasible arithmetics (Rutgers, NJ, 1996) DIMACS Ser. Discrete Math. Theoret. Comput. Sci., vol. 39, Amer. Math. Soc., Providence, RI, 1998, pp. 195-227. MR 1486622 (99c:03087)
  • [24] Alexis Maciel and Toniann Pitassi, A Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives, in: Proc. of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS 06), IEEE Computer Society Press, (August 2006).
  • [25] Toniann Pitassi, Paul Beame, and Russell Impagliazzo, Exponential lower bounds for the pigeonhole principle, Comput. Complexity 3 (1993), no. 2, 97-140. MR 1233662 (94f:03019),
  • [26] Pavel Pudlák, The lengths of proofs, Handbook of proof theory, Stud. Logic Found. Math., vol. 137, North-Holland, Amsterdam, 1998, pp. 547-637. MR 1640332 (99i:03073),
  • [27] Pavel Pudlák and Samuel R. Buss, How to lie without being (easily) convicted and the lengths of proofs in propositional calculus, Computer science logic (Kazimierz, 1994) Lecture Notes in Comput. Sci., vol. 933, Springer, Berlin, 1995, pp. 151-162. MR 1471224 (98f:03049),
  • [28] Alexander A. Razborov, Lower bounds on the dimension of schemes of bounded depth in a complete basis containing the logical addition function, Mat. Zametki 41 (1987), no. 4, 598-607, 623 (Russian). MR 897705 (89h:03110)
  • [29] Alexander A. Razborov, Lower bounds for the polynomial calculus, Comput. Complexity 7 (1998), no. 4, 291-324. MR 1691494 (2000e:03158),
  • [30] Roman 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.
  • [31] Andrew C.-C. Yao, Separating the polynomial-time hierarchy by oracles, in: Proc. 26th Ann. IEEE Symp. on Found. of Comp. Sci., (1985), pp. 1-10.

Similar Articles

Retrieve articles in Proceedings of the American Mathematical Society with MSC (2010): 03F20, 68Q17

Retrieve articles in all journals with MSC (2010): 03F20, 68Q17

Additional Information

Jan Krajíček
Affiliation: Faculty of Mathematics and Physics, Charles University, Sokolovská 83, Prague 8, CZ - 186 75, The Czech Republic

Received by editor(s): November 12, 2013
Received by editor(s) in revised form: November 21, 2013, December 2, 2013, and July 27, 2014
Published electronically: April 2, 2015
Communicated by: Mirna Dzamonja
Article copyright: © Copyright 2015 American Mathematical Society

American Mathematical Society