{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T09:04:24Z","timestamp":1758272664984,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Carl Zeiss Foundation"},{"DOI":"10.13039\/100000925","name":"John Templeton Foundation","doi-asserted-by":"publisher","award":["60842"],"award-info":[{"award-number":["60842"]}],"id":[{"id":"10.13039\/100000925","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394793","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"209-223","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution"],"prefix":"10.1145","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Friedrich-Schiller-Universit\u00e4t, Jena, Germany"}]},{"given":"Joshua","family":"Blinkhorn","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Friedrich-Schiller-Universit\u00e4t, Jena, Germany"}]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[{"name":"The Institute of Mathematical Sciences, HBNI Chennai, India"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"142","article-title":"Semi-Algebraic Proofs, IPS Lower Bounds and the tau - Conjecture: Can a Natural Number be Negative","volume":"26","author":"Alekseev Yaroslav","year":"2019","journal-title":"Electronic Colloquium on Computational Complexity"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0152-6"},{"volume-title":"Current Trends in Theoretical Computer Science: Entering the 21st Century","author":"Beame Paul","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200710069"},{"key":"e_1_3_2_1_6_1","unstructured":"Olaf Beyersdorff Joshua Blinkhorn and Luke Hinde. 2019. Size Cost and Capacity: A Semantic Technique for Hard Random QBFs. Logical Methods in Computer Science 15 1 (2019).  Olaf Beyersdorff Joshua Blinkhorn and Luke Hinde. 2019. Size Cost and Capacity: A Semantic Technique for Hard Random QBFs. Logical Methods in Computer Science 15 1 (2019)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2840728.2840740"},{"volume-title":"International Symposium on Theoretical Aspects of Computer Science (STACS) (Leibniz International Proceedings in Informatics (LIPIcs)), Ernst W","author":"Beyersdorff Olaf","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352155"},{"key":"e_1_3_2_1_10_1","unstructured":"Olaf Beyersdorff Leroy Chew Meena Mahajan and Anil Shukla. 2017. Feasible Interpolation for QBF Resolution Calculi. Logical Methods in Computer Science 13 (2017). Issue 2.  Olaf Beyersdorff Leroy Chew Meena Mahajan and Anil Shukla. 2017. Feasible Interpolation for QBF Resolution Calculi. Logical Methods in Computer Science 13 (2017). Issue 2."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3157053"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2016.11.011"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3378665"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.11.006"},{"volume-title":"International Conference on Theory and Practice of Satisfiability Testing (SAT) (Lecture Notes in Computer Science)","author":"Beyersdorff Olaf","key":"e_1_3_2_1_15_1"},{"volume-title":"Understanding Gentzen and Frege Systems for QBF. In Symposium on Logic in Computer Science (LICS), Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 146--155","year":"2016","author":"Beyersdorff Olaf","key":"e_1_3_2_1_16_1"},{"key":"e_1_3_2_1_17_1","unstructured":"A. Blake. 1937. Canonical expressions in boolean algebra. Ph.D. Dissertation. University of Chicago.  A. Blake. 1937. Canonical expressions in boolean algebra. Ph.D. Dissertation. University of Chicago."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90237-P"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(96)00077-4"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.009"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087534"},{"key":"e_1_3_2_1_22_1","unstructured":"Judith Clymo. [n.d.]. Ph.D. Dissertation. School of Computing University of Leeds. in preparation.  Judith Clymo. [n.d.]. Ph.D. Dissertation. School of Computing University of Leeds. in preparation."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2018.05.005"},{"key":"e_1_3_2_1_24_1","unstructured":"Stephen A. Cook and Phuong Nguyen. 2010. Logical Foundations of Proof Complexity. Cambridge University Press Cambridge.  Stephen A. Cook and Phuong Nguyen. 2010. Logical Foundations of Proof Complexity. Cambridge University Press Cambridge."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_3_2_1_26_1","volume-title":"International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science","volume":"9710","author":"Creignou Nadia","year":"2016"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-016-9501-2"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_47"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230742"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_3_2_1_31_1","unstructured":"J. H\u00e5stad. 1987. Computational Limitations of Small Depth Circuits. MIT Press Cambridge.  J. H\u00e5stad. 1987. Computational Limitations of Small Depth Circuits. MIT Press Cambridge."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Mikol\u00e1s Janota. 2016. On Q-Resolution and CDCL QBF Solving See [26] 402--418.  Mikol\u00e1s Janota. 2016. On Q-Resolution and CDCL QBF Solving See [26] 402--418.","DOI":"10.1007\/978-3-319-40970-2_25"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"volume-title":"International Joint Conference on Artificial Intelligence (IJCAI), Craig Boutilier (Ed.). AAAI Press, 836--841","year":"2009","author":"Kontchakov Roman","key":"e_1_3_2_1_35_1"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/225488"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-005-0203-0"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AMAI.0000012871.08577.0b"},{"key":"e_1_3_2_1_39_1","volume-title":"Evaluating QBF Solvers: Quantifier Alternations Matter. In International Conference on Principles and Practice of Constraint Programming (CP) (Lecture Notes in Computer Science), John N. Hooker (Ed.)","volume":"11008","author":"Lonsing Florian","year":"2018"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_9"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Florian Lonsing Uwe Egly and Martina Seidl. 2016. Q-Resolution with Generalized Axioms See [26] 435--452.  Florian Lonsing Uwe Egly and Martina Seidl. 2016. Q-Resolution with Generalized Axioms See [26] 435--452.","DOI":"10.1007\/978-3-319-40970-2_27"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.74"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815493.2815497"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2019.04.002"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01137685"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022607331053"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/28395.28404"},{"key":"e_1_3_2_1_50_1","unstructured":"Raymond M. Smullyan. 1995. First-order Logic. Dover Publications.  Raymond M. Smullyan. 1995. First-order Logic. Dover Publications."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/2578043","article-title":"Boolean Satisfiability","volume":"57","author":"Vardi Moshe Y.","year":"2014","journal-title":"Theory and Engineering. Commun. ACM"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"Saarbr\u00fccken Germany","acronym":"LICS '20"},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394793","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394793"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":51,"alternative-id":["10.1145\/3373718.3394793","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394793","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}