{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:47:29Z","timestamp":1781077649814,"version":"3.54.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Comput Complexity"],"published-print":{"date-parts":[[1996,9]]},"DOI":"10.1007\/bf01294258","type":"journal-article","created":{"date-parts":[[2005,3,24]],"date-time":"2005-03-24T22:12:22Z","timestamp":1111702342000},"page":"256-298","source":"Crossref","is-referenced-by-count":57,"title":["Proof complexity in algebraic systems and bounded depth Frege systems with modular counting"],"prefix":"10.1007","volume":"6","author":[{"given":"S.","family":"Buss","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R.","family":"Impagliazzo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J.","family":"Kraj\u00ed\u010dek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Pudl\u00e1k","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A. A.","family":"Razborov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J.","family":"Sgall","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"BF01294258_CR1","doi-asserted-by":"crossref","unstructured":"M. Ajtai, The complexity of the pigeonhole principle. InProceedings of the 29th IEEE Symposium on Foundations of Computer Science, 1988, 346\u2013355.","DOI":"10.1109\/SFCS.1988.21951"},{"key":"BF01294258_CR2","doi-asserted-by":"crossref","unstructured":"M. Ajtai, Parity and the pigeonhole principle. InFeasible Mathematics, ed.S. R. Buss and P. J. Scott, Birkh\u00e4user, 1990, 1\u201324.","DOI":"10.1007\/978-1-4612-3466-1_1"},{"key":"BF01294258_CR3","doi-asserted-by":"crossref","unstructured":"M. Ajtai, The independence of the modulop counting principle. InProceedings of the 26th ACM STOC, 1994, 402\u2013411.","DOI":"10.1145\/195058.195207"},{"key":"BF01294258_CR4","doi-asserted-by":"crossref","unstructured":"P. Beame, S. Cook, J. Edmonds, R. Impagliazzo, and T. Pitassi, The relative complexity ofNP search problems. InProceedings of the 27th ACM STOC, 1995, 303\u2013314.","DOI":"10.1145\/225058.225147"},{"key":"BF01294258_CR5","doi-asserted-by":"crossref","unstructured":"P. Beame, R. Impagliazzo, J. Kraj\u00ed\u010dek, T. Pitassi, and P. Pudl\u00e1k, Lower bounds on Hilbert's Nullstellensatz and propositional proofs. InProceedings of the 35th IEEE FOCS, 1994, 794\u2013806. Journal version to appear inProc. of the London Math. Soc.","DOI":"10.1109\/SFCS.1994.365714"},{"key":"BF01294258_CR6","unstructured":"P. Beame and T. Pitassi, Exponential separation between the matching principles and the pigeonhole principle. Submitted toAnnals of Pure and Applied Logic, 1993."},{"key":"BF01294258_CR7","doi-asserted-by":"crossref","unstructured":"P. Beame and S. Riis, More on the relative strength of counting principles. To appear inProceedings of the DIMACS workshop on Feasible Arithmetic and Complexity of Proofs, 1996.","DOI":"10.1090\/dimacs\/039\/02"},{"issue":"6","key":"BF01294258_CR8","doi-asserted-by":"crossref","first-page":"1161","DOI":"10.1137\/0221068","volume":"21","author":"S. Bellantoni","year":"1992","unstructured":"S. Bellantoni, T. Pitassi, andA. Urquhart, Approximation of small depth Frege proofs.SIAM Journal on Computing 21 (6) (1992), 1161\u20131179.","journal-title":"SIAM Journal on Computing"},{"key":"BF01294258_CR9","doi-asserted-by":"crossref","unstructured":"M. Bonet, T. Pitassi, and R. Raz, Lower bounds for cutting planes proofs with small coefficients. InProceedings of the 27th ACM STOC, 1995, 575\u2013584.","DOI":"10.1145\/225058.225275"},{"key":"BF01294258_CR10","unstructured":"Samuel R. Buss, A new exposition of the design for the housesitting principle. Manuscript, 1995a."},{"key":"BF01294258_CR11","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/BF02391554","volume":"34","author":"Samuel R. Buss","year":"1995","unstructured":"Samuel R. Buss, Some remarks on lengths of propositional proofs.Archive for Mathematical Logic 34 (1995b), 377\u2013394.","journal-title":"Archive for Mathematical Logic"},{"issue":"4","key":"BF01294258_CR12","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"V. Chv\u00e1tal andE. Szemer\u00e9di, Many hard examples for resolution.Journal of the ACM 35(4) (1988), 759\u2013768.","journal-title":"Journal of the ACM"},{"key":"BF01294258_CR13","doi-asserted-by":"crossref","unstructured":"M. Clegg, J. Edmonds, and R. Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability. InProceedings of the 28th ACM STOC, 1996, 174\u2013183.","DOI":"10.1145\/237814.237860"},{"issue":"1","key":"BF01294258_CR14","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. A. Cook","year":"1979","unstructured":"S. A. Cook andA. R. Reckhow, The relative efficiency of propositional proof systems.Journal of Symbolic Logic 44(1) (1979), 36\u201350.","journal-title":"Journal of Symbolic Logic"},{"key":"BF01294258_CR15","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken, The intractability of resolution.Theoretical Computer Science 39 (1985), 297\u2013308.","journal-title":"Theoretical Computer Science"},{"key":"BF01294258_CR16","unstructured":"Johan H\u00e5stad, Almost optimal lower bounds for small depth circuits. InRandomness and Computation (Advances in Computing Research, Vol. 5), ed.S. Micali, 143\u2013170. JAI Press, 1989."},{"key":"BF01294258_CR17","unstructured":"R. Impagliazzo, The sequential ideal generation proof system. Unpublished note, 1995."},{"issue":"1","key":"BF01294258_CR18","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2275250","volume":"59","author":"J. Kraj\u00ed\u010dek","year":"1994","unstructured":"J. Kraj\u00ed\u010dek, Lower bounds to the size of constant-depth propositional proofs.Journal of Symbolic Logic 59(1) (1994a), 73\u201386.","journal-title":"Journal of Symbolic Logic"},{"key":"BF01294258_CR19","unstructured":"J. Kraj\u00ed\u010dek, Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. To appear inJournal of Symbolic Logic, 1994b."},{"key":"BF01294258_CR20","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek,Bounded arithmetic, propositional logic and complexity theory. Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, 1995.","DOI":"10.1017\/CBO9780511529948"},{"key":"BF01294258_CR21","first-page":"56","volume":"2","author":"J. Kraj\u00ed\u010dek","year":"1996","unstructured":"J. Kraj\u00ed\u010dek, A fundamental problem of mathematical logic.Annals of the Kurt G\u00f6del Society, Collegium Logicum, Vol.2, Springer-Verlag, 1996, 56\u201364.","journal-title":"Annals of the Kurt G\u00f6del Society"},{"key":"BF01294258_CR22","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-94-017-0487-8_4","volume-title":"Logic and Scientific Methods","author":"J. Kraj\u00ed\u010dek","year":"1997","unstructured":"J. Kraj\u00ed\u010dek, On methods for proving lower bounds in propositional logic. InLogic and Scientific Methods, eds. M. L. Dalla Chiara et al., (Vol. 1 of Proc. of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 19\u201325, 1995), Synthese Library, Vol.259, Kluwer Academic Publ., Dordrecht, 1997, 69\u201383."},{"issue":"1","key":"BF01294258_CR23","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1002\/rsa.3240070103","volume":"7","author":"J. Kraj\u00ed\u010dek","year":"1995","unstructured":"J. Kraj\u00ed\u010dek, P. Pudl\u00e1k, andA. R. Woods, Exponential lower bounds to the size of bounded depth Frege proofs of the pigeonhole principle.Random Structures and Algorithms 7(1) (1995), 15\u201339.","journal-title":"Random Structures and Algorithms"},{"issue":"4","key":"BF01294258_CR24","doi-asserted-by":"crossref","first-page":"1235","DOI":"10.1017\/S0022481200028061","volume":"53","author":"J. B. Paris","year":"1988","unstructured":"J. B. Paris, A. J. Wilkie, andA. R. Woods, Provability of the pigeonhole principle and the existence of infinitely many primes.Journal of Symbolic Logic 53(4) (1988), 1235\u20131244.","journal-title":"Journal of Symbolic Logic"},{"key":"BF01294258_CR25","doi-asserted-by":"crossref","unstructured":"T. Pitassi, Algebraic Propositional Proof Systems. To appear in the proceedings volume of the DIMACS workshop onFinite Models and Descriptive Complexity, held January 14\u201317, 1996.","DOI":"10.1090\/dimacs\/031\/07"},{"key":"BF01294258_CR26","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF01200117","volume":"3","author":"T. Pitassi","year":"1993","unstructured":"T. Pitassi, P. Beame, andR. Impagliazzo, Exponential lower bounds for the pigeonhole principle.computational complexity 3 (1993), 97\u2013140.","journal-title":"computational complexity"},{"key":"BF01294258_CR27","unstructured":"P. Pudl\u00e1k, The lengths of proofs. To appear inHandbook of Proof Theory, 1995a."},{"key":"BF01294258_CR28","unstructured":"P. Pudl\u00e1k, Lower bounds for resolution and cutting planes proofs and monotone computations. To appear inJournal of Symbolic Logic, 1995b."},{"key":"BF01294258_CR29","doi-asserted-by":"crossref","unstructured":"A. A. Razborov, On the method of approximation. InProceedings of the 21st ACM Symposium on Theory of Computing, 1989, 167\u2013176.","DOI":"10.1145\/73007.73023"},{"key":"BF01294258_CR30","doi-asserted-by":"crossref","unstructured":"A. Razborov, Lower bounds for the polynomial calculus. To appear incomputational complexity 7 (1998).","DOI":"10.1007\/s000370050013"},{"key":"BF01294258_CR31","unstructured":"R. A. Reckhow, On the lengths of proofs in the propositional calculus. Technical Report 87, University of Toronto, 1976."},{"key":"BF01294258_CR32","doi-asserted-by":"crossref","unstructured":"S. Riis,Independence in Bounded Arithmetic. PhD thesis, Oxford University, 1993.","DOI":"10.7146\/brics.v1i23.21644"},{"key":"BF01294258_CR33","volume-title":"Count(q) does not imply Count(p)","author":"S. Riis","year":"1994","unstructured":"S. Riis, Count(q) does not imply Count(p). Technical Report RS-94-21, Basic Research in Computer Science Center, Aarhus, Denmark, 1994."},{"key":"BF01294258_CR34","doi-asserted-by":"crossref","unstructured":"R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity. InProceedings of the 19th ACM Symposium on Theory of Computing, 1987, 77\u201382.","DOI":"10.1145\/28395.28404"},{"issue":"1","key":"BF01294258_CR35","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"A. Urquhart, Hard examples for resolution.Journal of the ACM 34(1) (1987), 209\u2013219.","journal-title":"Journal of the ACM"},{"key":"BF01294258_CR36","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"A. Urquhart, The complexity of propositional proofs.Bulletin of Symbolic Logic 1 (1995), 425\u2013467.","journal-title":"Bulletin of Symbolic Logic"},{"key":"BF01294258_CR37","unstructured":"A. Wigderson, The fusion method for lower bounds in circuit complexity. InCombinatorics, Paul Erd\u0151s is Eighty (Vol. 1) (1993), 453\u2013468."}],"container-title":["Computational Complexity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01294258.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01294258\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01294258","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T17:34:21Z","timestamp":1735407261000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01294258"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["BF01294258"],"URL":"https:\/\/doi.org\/10.1007\/bf01294258","relation":{},"ISSN":["1016-3328","1420-8954"],"issn-type":[{"value":"1016-3328","type":"print"},{"value":"1420-8954","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}