{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:39:51Z","timestamp":1750307991501,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2006,4,1]],"date-time":"2006-04-01T00:00:00Z","timestamp":1143849600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,4]]},"abstract":"<jats:p>\n            We show that constant-depth Frege systems with counting axioms modulo\n            <jats:italic>m<\/jats:italic>\n            polynomially simulate Nullstellensatz refutations modulo\n            <jats:italic>m<\/jats:italic>\n            . Central to this is a new definition of reducibility from propositional formulas to systems of polynomials. Using our definition of reducibility, most previously studied propositional formulas reduce to their polynomial translations. When combined with a previous result of the authors, this establishes the first size separation between Nullstellensatz and polynomial calculus refutations. We also obtain new upper bounds on refutation sizes for certain CNFs in constant-depth Frege with counting axioms systems.\n          <\/jats:p>","DOI":"10.1145\/1131313.1131314","type":"journal-article","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:14:26Z","timestamp":1153836866000},"page":"199-218","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations"],"prefix":"10.1145","volume":"7","author":[{"given":"Russell","family":"Impagliazzo","sequence":"first","affiliation":[{"name":"University of California, San Diego, CA"}]},{"given":"Nathan","family":"Segerlind","sequence":"additional","affiliation":[{"name":"University of California, San Diego, Princeton, NJ"}]}],"member":"320","published-online":{"date-parts":[[2006,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3466-1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01302964"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/195058.195207"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/795666.796580"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(96)83747-X"},{"key":"e_1_2_1_7_1","first-page":"66","article-title":"Propositional proof complexity: Past, present, and future","volume":"65","author":"Beame P.","year":"1998","unstructured":"Beame , P. and Pitassi , T. 1998 . Propositional proof complexity: Past, present, and future . Bull. European Assoc. Theoret. Comput. Science 65 , 66 -- 89 . Beame, P. and Pitassi, T. 1998. Propositional proof complexity: Past, present, and future. Bull. European Assoc. Theoret. Comput. Science 65, 66--89.","journal-title":"Bull. European Assoc. Theoret. Comput. Science"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Beame P. and Riis S. 1998. More one the relative strength of counting principles. In P. Beame and S. Buss Eds. Proof Complexity and Feasible Arithmetics 13--35. American Mathematical Society.  Beame P. and Riis S. 1998. More one the relative strength of counting principles. In P. Beame and S. Buss Eds. Proof Complexity and Feasible Arithmetics 13--35. American Mathematical Society.","DOI":"10.1090\/dimacs\/039\/02"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-002-0172-5"},{"volume-title":"Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science. 415--421","author":"Ben-Sasson E.","key":"e_1_2_1_10_1","unstructured":"Ben-Sasson , E. and Impagliazzo , R . 1999. Random CNFs are hard for the polynomial calculus . In Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science. 415--421 . Ben-Sasson, E. and Impagliazzo, R. 1999. Random CNFs are hard for the polynomial calculus. In Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science. 415--421."},{"volume-title":"Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science. 422--431","author":"Bonet M. L.","key":"e_1_2_1_11_1","unstructured":"Bonet , M. L. and Galesi , N . 1999. A study of proof search algorithms for resolution and polynomial calculus . In Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science. 422--431 . Bonet, M. L. and Galesi, N. 1999. A study of proof search algorithms for resolution and polynomial calculus. In Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science. 422--431."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-002-0171-6"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01294258"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1585"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"volume-title":"Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science. 200--209","author":"Impagliazzo R.","key":"e_1_2_1_19_1","unstructured":"Impagliazzo , R. and Segerlind , N . 2001. Counting axioms do not polynomially simulate counting gates (extended abstract) . In Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science. 200--209 . Impagliazzo, R. and Segerlind, N. 2001. Counting axioms do not polynomially simulate counting gates (extended abstract). In Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science. 200--209."},{"volume-title":"Propositional Logic and Complexity Theory","author":"Kraj\u00ed\u010dek J.","key":"e_1_2_1_20_1","unstructured":"Kraj\u00ed\u010dek , J. 1995. Bounded Arithmetic , Propositional Logic and Complexity Theory . Cambridge University Press . Kraj\u00ed\u010dek, J. 1995. Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2307\/2687774"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"volume-title":"Descriptive Complexity and Finite Models","author":"Pitassi T.","key":"e_1_2_1_23_1","unstructured":"Pitassi , T. 1997. Algebraic propositional proof systems . In N. Immerman and P. G. Kolaitis, Eds. Descriptive Complexity and Finite Models vol. 31 DIMACS : Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society . Pitassi, T. 1997. Algebraic propositional proof systems. In N. Immerman and P. G. Kolaitis, Eds. Descriptive Complexity and Finite Models vol. 31 DIMACS: Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"volume-title":"Handbook of Proof Theory","author":"Pudl\u00e1k P.","key":"e_1_2_1_25_1","unstructured":"Pudl\u00e1k , P. 1998. The lengths of proofs . In S. R. Buss, Eds. Handbook of Proof Theory . Elsevier North-Holland . 547--637. Pudl\u00e1k, P. 1998. The lengths of proofs. In S. R. Buss, Eds. Handbook of Proof Theory. Elsevier North-Holland. 547--637."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(97)00029-8"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Tseitin G. 1970. On the complexity of proofs in propositional logics. Seminars in Mathematics 8.  Tseitin G. 1970. On the complexity of proofs in propositional logics. Seminars in Mathematics 8.","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1131313.1131314","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1131313.1131314","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:16Z","timestamp":1750259176000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1131313.1131314"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["10.1145\/1131313.1131314"],"URL":"https:\/\/doi.org\/10.1145\/1131313.1131314","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,4]]},"assertion":[{"value":"2006-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}