{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2021,5,12]],"date-time":"2021-05-12T06:43:21Z","timestamp":1620801801791},"reference-count":34,"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":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"John Templeton Foundation under the Project The Limits of Theorem Proving"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2015,6,30]]},"abstract":"\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 n<\/jats:italic>\n ) space lower bounds in PC\/PCR for random\n k<\/jats:italic>\n -CNFs (\n k<\/jats:italic>\n \u2265 4) in\n 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","source":"Crossref","is-referenced-by-count":6,"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"}]},{"given":"Nicola","family":"Galesi","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Roma, Italy"}]}],"member":"320","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","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_6_1","unstructured":"Eli Ben-Sasson. 2001. Expansion in proof complexity. Ph.D. dissertation Hebrew University. Eli Ben-Sasson. 2001. Expansion in proof complexity. Ph.D. dissertation Hebrew University."},{"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"},{"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_12_1","unstructured":"Archie Blake. 1937. Canonical expressions in Boolean algebra. Ph.D. dissertation University of Chicago. Archie Blake. 1937. Canonical expressions in Boolean algebra. Ph.D. dissertation University of Chicago."},{"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"},{"key":"e_1_2_1_20_1","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","edition":"2"},{"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","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\/pdf\/10.1145\/2699438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,1]],"date-time":"2021-03-01T21:49:13Z","timestamp":1614635353000},"score":1,"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,30]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6,30]]}},"alternative-id":["10.1145\/2699438"],"URL":"http:\/\/dx.doi.org\/10.1145\/2699438","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":["Artificial Intelligence","Hardware and Architecture","Information Systems","Control and Systems Engineering","Software"],"published":{"date-parts":[[2015,6,30]]}}}