{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:18:45Z","timestamp":1750306725883,"version":"3.41.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T00:00:00Z","timestamp":1431302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Sciences and Engineering Research Council"},{"name":"National Science Foundation","award":["DMS-1128155"],"award-info":[{"award-number":["DMS-1128155"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2015,5,11]]},"abstract":"<jats:p>\n            We give a general transformation that turns polynomial-size Frege proofs into subexponential-size AC\n            <jats:sup>0<\/jats:sup>\n            -Frege proofs. This indicates that proving truly exponential lower bounds for AC\n            <jats:sup>0<\/jats:sup>\n            -Frege is hard, as it is a long-standing open problem to prove superpolynomial lower bounds for Frege. Our construction is optimal for proofs of formulas of unbounded depth.\n          <\/jats:p>\n          <jats:p>As a consequence of our main result, we are able to shed some light on the question of automatizability for bounded-depth Frege systems. First, we present a simpler proof of the results of Bonet et al. showing that under cryptographic assumptions, bounded-depth Frege proofs are not automatizable. Second, we show that because our proof is more general, under the right cryptographic assumptions, it could resolve the automatizability question for lower-depth Frege systems.<\/jats:p>","DOI":"10.1145\/2656209","type":"journal-article","created":{"date-parts":[[2015,5,12]],"date-time":"2015-05-12T12:18:00Z","timestamp":1431433080000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Exponential Lower Bounds for AC\n            <sup>0<\/sup>\n            -Frege Imply Superpolynomial Frege Lower Bounds"],"prefix":"10.1145","volume":"7","author":[{"given":"Yuval","family":"Filmus","sequence":"first","affiliation":[{"name":"University of Toronto, NJ"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toniann","family":"Pitassi","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahul","family":"Santhanam","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,5,11]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.5555\/874063.875574"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1137\/060664537"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1016\/j.ic.2011.01.003"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/129712.129733"},{"volume-title":"Are there hard examples for Frege systems&quest","author":"Bonet Maria Luisa","unstructured":"Maria Luisa Bonet , Samuel R. Buss , and Toniann Pitassi . 1995. Are there hard examples for Frege systems&quest ; In Feasible Mathematics II, P. Clote and J. Remmel (Eds.). Birkh\u00e4user , Boston, MA , 30--56. Maria Luisa Bonet, Samuel R. Buss, and Toniann Pitassi. 1995. Are there hard examples for Frege systems&quest; In Feasible Mathematics II, P. Clote and J. Remmel (Eds.). Birkh\u00e4user, Boston, MA, 30--56.","key":"e_1_2_1_6_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1007\/s00037-004-0183-5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1137\/S0097539798353230"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/321812.321815"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.2307\/2273826"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.2307\/2273702"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1305\/ndjfl\/1040046140"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the Annual Conference on Computer Science Logic (CSL\u201913)","author":"Ghasemloo Kaveh","year":"2013","unstructured":"Kaveh Ghasemloo and Stephen A. Cook . 2013. Theories for subexponential-size bounded-depth Frege proofs . In Proceedings of the Annual Conference on Computer Science Logic (CSL\u201913) . 296--315. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.CSL. 2013 .296 10.4230\/LIPIcs.CSL.2013.296 Kaveh Ghasemloo and Stephen A. Cook. 2013. Theories for subexponential-size bounded-depth Frege proofs. In Proceedings of the Annual Conference on Computer Science Logic (CSL\u201913). 296--315. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.CSL.2013.296"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1016\/0304-3975(85)90144-6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.2307\/2275250"},{"volume-title":"Propositional Logic, and Complexity Theory","author":"Kraj\u00ed\u010dek Jan","unstructured":"Jan Kraj\u00ed\u010dek . 1995. Bounded Arithmetic , Propositional Logic, and Complexity Theory . Cambridge University Press , New York, NY . Jan Kraj\u00ed\u010dek. 1995. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press, New York, NY.","key":"e_1_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.2307\/2275541"},{"volume-title":"Forcing with Random Variables and Proof Complexity","author":"Kraj\u00ed\u010dek Jan","unstructured":"Jan Kraj\u00ed\u010dek . 2011. Forcing with Random Variables and Proof Complexity . London Mathematical Society , London, United Kingdom. Jan Kraj\u00ed\u010dek. 2011. Forcing with Random Variables and Proof Complexity. London Mathematical Society, London, United Kingdom.","key":"e_1_2_1_20_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1002\/rsa.3240070103"},{"unstructured":"Leonid A. Levin. 1973. Universal sequential search problems. Problems of Information Transmission (translated from Russian) 9 3 115--116.  Leonid A. Levin. 1973. Universal sequential search problems. Problems of Information Transmission (translated from Russian) 9 3 115--116.","key":"e_1_2_1_22_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.2168\/LMCS-9(1:16)2013"},{"unstructured":"V. A. Nepomnja\u0161\u010dij. 1970. Rudimentary predicates and Turing calculations. Soviet Mathematics Doklady 1462--1465.  V. A. Nepomnja\u0161\u010dij. 1970. Rudimentary predicates and Turing calculations. Soviet Mathematics Doklady 1462--1465.","key":"e_1_2_1_24_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1016\/j.artint.2010.10.002"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1007\/BF01200117"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1145\/800061.808733"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 4th Hawaii Symposium on System Sciences. IEEE","author":"Spira P. M.","year":"1971","unstructured":"P. M. Spira . 1971 . On time-hardware complexity tradeoffs for Boolean functions . In Proceedings of the 4th Hawaii Symposium on System Sciences. IEEE , Los Alamitos, CA, 525--527. P. M. Spira. 1971. On time-hardware complexity tradeoffs for Boolean functions. In Proceedings of the 4th Hawaii Symposium on System Sciences. IEEE, Los Alamitos, CA, 525--527."}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2656209","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2656209","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:37Z","timestamp":1750231177000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2656209"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,11]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,5,11]]}},"alternative-id":["10.1145\/2656209"],"URL":"https:\/\/doi.org\/10.1145\/2656209","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"type":"print","value":"1942-3454"},{"type":"electronic","value":"1942-3462"}],"subject":[],"published":{"date-parts":[[2015,5,11]]},"assertion":[{"value":"2013-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-05-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}