{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:19:44Z","timestamp":1783009184388,"version":"3.54.5"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T00:00:00Z","timestamp":1586044800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2020,4,30]]},"abstract":"<jats:p>\n            We define and investigate Frege systems for quantified Boolean formulas (QBF). For these new proof systems, we develop a lower bound technique that directly lifts circuit lower bounds for a circuit class\n            <jats:italic>C<\/jats:italic>\n            to the QBF Frege system operating with lines from\n            <jats:italic>C<\/jats:italic>\n            . Such a direct transfer from circuit to proof complexity lower bounds has often been postulated for propositional systems but had not been formally established in such generality for any proof systems prior to this work.\n          <\/jats:p>\n          <jats:p>\n            This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponential lower bound for QBF Frege systems operating with AC\n            <jats:sup>0<\/jats:sup>\n            [\n            <jats:italic>p<\/jats:italic>\n            ] circuits. In contrast, any non-trivial lower bound for propositional AC\n            <jats:sup>0<\/jats:sup>\n            [\n            <jats:italic>p<\/jats:italic>\n            ]-Frege constitutes a major open problem.\n          <\/jats:p>\n          <jats:p>\n            Improving these lower bounds to unrestricted QBF Frege tightly corresponds to\n            <jats:italic>the<\/jats:italic>\n            major problems in circuit complexity and propositional proof complexity. In particular, proving a lower bound for QBF Frege systems operating with arbitrary P\/poly circuits is equivalent to either showing a lower bound for P\/poly or for propositional extended Frege (which operates with P\/poly circuits).\n          <\/jats:p>\n          <jats:p>We also compare our new QBF Frege systems to standard sequent calculi for QBF and establish a correspondence to intuitionistic bounded arithmetic.<\/jats:p>","DOI":"10.1145\/3381881","type":"journal-article","created":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T12:03:23Z","timestamp":1586088203000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Frege Systems for Quantified Boolean Logic"],"prefix":"10.1145","volume":"67","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"University of Jena, Jena, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilario","family":"Bonacina","sequence":"additional","affiliation":[{"name":"UPC Barcelona, Barcelona, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leroy","family":"Chew","sequence":"additional","affiliation":[{"name":"University of Leeds"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"Pich","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,4,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01302964"},{"key":"e_1_2_1_2_1","volume-title":"Computational Complexity\u2014A Modern Approach","author":"Arora Sanjeev"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0152-6"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914)","author":"Balabanov Valeriy"},{"key":"e_1_2_1_5_1","volume-title":"Current Trends in Theoretical Computer Science: Entering the 21st Century","author":"Beame Paul"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_7_1","first-page":"1","article-title":"QBF-based formal verification: Experience and perspectives","volume":"5","author":"Benedetti Marco","year":"2008","journal-title":"J. Satis. Boolean Model. Comput."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200710069"},{"key":"e_1_2_1_9_1","volume-title":"cost, and capacity: A semantic technique for hard random QBFs. Log. Methods Comput. Sci. 15, 1","author":"Beyersdorff Olaf","year":"2019"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2840728.2840740"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44465-8_8"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS\u201915)","author":"Beyersdorff Olaf","year":"2015"},{"key":"e_1_2_1_13_1","volume-title":"Beyond NP, Papers from the 2016 AAAI Workshop","author":"Beyersdorff Olaf"},{"key":"e_1_2_1_14_1","volume-title":"Feasible interpolation for QBF resolution calculi. Log. Methods Comput. Sci. 13","author":"Beyersdorff Olaf","year":"2017"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.08.002"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 37th IARCS Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201917)","author":"Beyersdorff Olaf","year":"2017"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_13"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933597"},{"key":"e_1_2_1_20_1","first-page":"1","article-title":"Non-automatizability of bounded-depth Frege proofs","volume":"13","author":"Bonet Maria Luisa","year":"2004","journal-title":"Computat. Complex."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539798353230"},{"key":"e_1_2_1_22_1","volume-title":"Boppana and Michael Sipser","author":"Ravi","year":"1990"},{"key":"e_1_2_1_23_1","unstructured":"Samuel R. Buss. 1986a. Bounded Arithmetic. Bibliopolis Napoli.  Samuel R. Buss. 1986a. Bounded Arithmetic. Bibliopolis Napoli."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16486-3_91"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.009"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01845704"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00002-0"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-005-0282-2"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 7th ACM Symposium on Theory of Computing. 83--97","author":"Cook Stephen A.","year":"1975"},{"key":"e_1_2_1_31_1","volume-title":"Cook and Phuong Nguyen","author":"Stephen","year":"2010"},{"key":"e_1_2_1_32_1","first-page":"169","article-title":"The relative efficiency of propositional proof systems","volume":"6","author":"Cook Stephen A.","year":"1979","journal-title":"J. Symb. Log."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183283"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90044-E"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"e_1_2_1_36_1","unstructured":"Martin Dowd. 1985. Model-Theoretic Aspects of P#NP. (1985). Unpublished manuscript. https:\/\/www.researchgate.net\/publication\/337090251_Model_Theoretic_Aspects_of_P_N_P.  Martin Dowd. 1985. Model-Theoretic Aspects of P#NP. (1985). Unpublished manuscript. https:\/\/www.researchgate.net\/publication\/337090251_Model_Theoretic_Aspects_of_P_N_P."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_9"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-016-9501-2"},{"key":"e_1_2_1_39_1","first-page":"68","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen Gerhard","year":"1935","journal-title":"Math. Zeit."},{"key":"e_1_2_1_40_1","unstructured":"Kaveh Ghasemloo and J\u00e1n Pich. 2013. A note on natural proofs and intuitionism. (2013). Retrieved from karlin.mff.cuni.cz\/\u223cpich\/natcons.pdf.  Kaveh Ghasemloo and J\u00e1n Pich. 2013. A note on natural proofs and intuitionism. (2013). Retrieved from karlin.mff.cuni.cz\/\u223cpich\/natcons.pdf."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201911)","author":"Goultiaeva Alexandra","year":"2011"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/12130.12132"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9390-4"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.09.013"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.10.005"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.201020093"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531024"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/225488"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275541"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274765"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19900360106"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2674"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321882"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269958"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01137685"},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence (AAAI\u201907)","author":"Rintanen Jussi","year":"2007"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022607331053"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/28395.28404"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_47"},{"key":"e_1_2_1_69_1","volume-title":"Introduction to Circuit Complexity\u2014A Uniform Approach","author":"Vollmer Heribert"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3381881","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3381881","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:33:07Z","timestamp":1750199587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3381881"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,5]]},"references-count":67,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4,30]]}},"alternative-id":["10.1145\/3381881"],"URL":"https:\/\/doi.org\/10.1145\/3381881","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,5]]},"assertion":[{"value":"2016-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-04-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}