{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:48Z","timestamp":1750306608069,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,6,30]],"date-time":"2015-06-30T00:00:00Z","timestamp":1435622400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"John Templeton Foundation under the Project The Limits of Theorem Proving"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2015,6,30]]},"abstract":"<jats:p>\n            Algebraic proof systems, such as Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR), refute contradictions using polynomials. Space complexity for such systems measures the number of distinct monomials to be kept in memory while verifying a proof. We introduce a new combinatorial framework for proving space lower bounds in algebraic proof systems. As an immediate application, we obtain the space lower bounds previously provided for PC\/PCR [Alekhnovich et al. 2002; Filmus et al. 2012]. More importantly, using our approach in its full potential, we prove \u03a9(\n            <jats:italic>n<\/jats:italic>\n            ) space lower bounds in PC\/PCR for random\n            <jats:italic>k<\/jats:italic>\n            -CNFs (\n            <jats:italic>k<\/jats:italic>\n            \u2265 4) in\n            <jats:italic>n<\/jats:italic>\n            variables, thus solving an open problem posed in Alekhnovich et al. [2002] and Filmus et al. [2012]. Our method also applies to the Graph Pigeonhole Principle, which is a variant of the Pigeonhole Principle defined over a constant (left) degree expander graph.\n          <\/jats:p>","DOI":"10.1145\/2699438","type":"journal-article","created":{"date-parts":[[2015,7,6]],"date-time":"2015-07-06T14:04:16Z","timestamp":1436191456000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A Framework for Space Complexity in Algebraic Proof Systems"],"prefix":"10.1145","volume":"62","author":[{"given":"Ilario","family":"Bonacina","sequence":"first","affiliation":[{"name":"Sapienza University of Rome, Roma, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Galesi","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Roma, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,6,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_2_1_2_1","first-page":"18","article-title":"Lower bounds for polynomial calculus: Non-binomial case","volume":"242","author":"Alekhnovich Michael","year":"2003","unstructured":"Michael Alekhnovich and Alexander A. Razborov . 2003 . Lower bounds for polynomial calculus: Non-binomial case . In Proceedings of the Steklov Institute of Mathematics , Vol. 242. 18 -- 35 . Michael Alekhnovich and Alexander A. Razborov. 2003. Lower bounds for polynomial calculus: Non-binomial case. In Proceedings of the Steklov Institute of Mathematics, Vol. 242. 18--35.","journal-title":"Proceedings of the Steklov Institute of Mathematics"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/972639.972645"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/874062.875477"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.10089"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-010-0293-1"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of ICS, Bernard Chazelle (Ed.)","author":"Ben-Sasson Eli","year":"2011","unstructured":"Eli Ben-Sasson and Jakob Nordstr\u00f6m . 2011 . Understanding space in proof complexity: Separations and trade-offs via substitutions . In Proceedings of ICS, Bernard Chazelle (Ed.) , Tsinghua University Press, 401--416. Eli Ben-Sasson and Jakob Nordstr\u00f6m. 2011. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proceedings of ICS, Bernard Chazelle (Ed.), Tsinghua University Press, 401--416."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_11_1","unstructured":"Patrick Bennet Ilario Bonacina Nicola Galesi Tony Huynh Mike Molloy and Paul Wollan. 2015. Space proof complexity for random 3-CNFs. arXiv. (2015) http:\/\/arxiv.org\/abs\/1503.01613.  Patrick Bennet Ilario Bonacina Nicola Galesi Tony Huynh Mike Molloy and Paul Wollan. 2015. Space proof complexity for random 3-CNFs. arXiv. (2015) http:\/\/arxiv.org\/abs\/1503.01613."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422436.2422486"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2014.74"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01294258"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"edition":"2","volume-title":"David A. Cox, John Little, and Donal O'Shea. 1997. Ideals, Varieties, and Algorithms - An Introduction to Computational Algebraic Geometry and Commutative Algebra","key":"e_1_2_1_20_1","unstructured":"David A. Cox, John Little, and Donal O'Shea. 1997. Ideals, Varieties, and Algorithms - An Introduction to Computational Algebraic Geometry and Commutative Algebra 2 nd Ed., Springer . I--XIII, 1--536. David A. Cox, John Little, and Donal O'Shea. 1997. Ideals, Varieties, and Algorithms - An Introduction to Computational Algebraic Geometry and Commutative Algebra 2nd Ed., Springer. I--XIII, 1--536."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.004"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39206-1_37"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2012.27"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-009-9195-5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838556"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_2_1_28_1","unstructured":"Jan Kraj\u00ed\u010dek. 2009. Propositional proof complexity I. Manuscript available at author's webpage.  Jan Kraj\u00ed\u010dek. 2009. Propositional proof complexity I. Manuscript available at author's webpage."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1137\/060668250"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2013.v009a014"},{"key":"e_1_2_1_31_1","first-page":"279","article-title":"Algebraic models of computation and interpolation for algebraic proof systems. DIMACS Series in Discrete Math","volume":"39","author":"Pudl\u00e1k Pavel","year":"1998","unstructured":"Pavel Pudl\u00e1k and Ji\u0159\u00ed Sgall . 1998 . Algebraic models of computation and interpolation for algebraic proof systems. DIMACS Series in Discrete Math . Theoret. Comput. Sci. 39 , 279 -- 295 . Pavel Pudl\u00e1k and Ji\u0159\u00ed Sgall. 1998. Algebraic models of computation and interpolation for algebraic proof systems. DIMACS Series in Discrete Math. Theoret. Comput. Sci. 39, 279--295.","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"e_1_2_1_33_1","unstructured":"Alexander A. Razborov. 2003. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Manuscript available at author's webpage.  Alexander A. Razborov. 2003. Pseudorandom generators hard for k -DNF resolution and polynomial calculus resolution. Manuscript available at author's webpage."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699438","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2699438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:58Z","timestamp":1750227418000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699438"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,30]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6,30]]}},"alternative-id":["10.1145\/2699438"],"URL":"https:\/\/doi.org\/10.1145\/2699438","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2015,6,30]]},"assertion":[{"value":"2013-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-06-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}