{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:11:09Z","timestamp":1753888269909,"version":"3.37.3"},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T00:00:00Z","timestamp":1634083200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T00:00:00Z","timestamp":1634083200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["DTG"],"award-info":[{"award-number":["DTG"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"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"}]},{"DOI":"10.13039\/100007569","name":"Carl-Zeiss-Stiftung","doi-asserted-by":"publisher","award":["Grant for returning scientists"],"award-info":[{"award-number":["Grant for returning scientists"]}],"id":[{"id":"10.13039\/100007569","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["BE 4209\/3-1"],"award-info":[{"award-number":["BE 4209\/3-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3\u20134):117\u2013134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods\u201424th international conference, (TABLEAUX\u201915), pp 185\u2013200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI\u201917), pp 4919\u20134923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover\u2013Delayer games, which can be used to establish \u201cgenuine\u201d modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrube\u0161 (Ann Pure Appl Log 157(2\u20133):194\u2013205, 2009) and obtain a \u201cgenuinely\u201d modal separation.<\/jats:p>","DOI":"10.1007\/s10817-021-09609-9","type":"journal-article","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T21:35:22Z","timestamp":1634160922000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Proof Complexity of Modal Resolution"],"prefix":"10.1007","volume":"66","author":[{"given":"Sarah","family":"Sigley","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2870-1648","authenticated-orcid":false,"given":"Olaf","family":"Beyersdorff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,13]]},"reference":[{"issue":"5","key":"9609_CR1","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1093\/logcom\/11.5.717","volume":"11","author":"C Areces","year":"2001","unstructured":"Areces, C., de Rijke, M., de Nivelle, H.: Resolution in modal, description and hybrid logic. J. Log. Comput. 11(5), 717\u2013736 (2001)","journal-title":"J. Log. Comput."},{"issue":"1","key":"9609_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-010-9167-0","volume":"46","author":"C Areces","year":"2011","unstructured":"Areces, C., Gor\u00edn, D.: Resolution with order and selection for hybrid logics. J. Autom. Reason. 46(1), 1\u201342 (2011)","journal-title":"J. Autom. Reason."},{"key":"9609_CR3","doi-asserted-by":"crossref","unstructured":"Atserias, A., Bonacina, I., de\u00a0Rezende, S.F., Lauria, M., Nordstr\u00f6m, J., Razborov, A.A.: Clique is hard on average for regular resolution. In: Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing (STOC), pp. 866\u2013877 (2018)","DOI":"10.1145\/3188745.3188856"},{"issue":"3","key":"9609_CR4","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1006249507577","volume":"24","author":"P Balsiger","year":"2000","unstructured":"Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. J. Autom. Reason. 24(3), 297\u2013317 (2000)","journal-title":"J. Autom. Reason."},{"key":"9609_CR5","doi-asserted-by":"crossref","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res.: JAIR 22, 319\u2013351 (2004)","DOI":"10.1613\/jair.1410"},{"key":"9609_CR6","first-page":"42","volume-title":"Current Trends in Theoretical Computer Science: Entering the 21st Century","author":"P Beame","year":"2001","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: past, present, and future. In: Paun, G., Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science: Entering the 21st Century, pp. 42\u201370. World Scientific Publishing, Singapore (2001)"},{"issue":"2","key":"9609_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow\u2013resolution made simple. J. ACM 48(2), 149\u2013169 (2001)","journal-title":"J. ACM"},{"issue":"2","key":"9609_CR8","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1002\/malq.200710069","volume":"55","author":"O Beyersdorff","year":"2009","unstructured":"Beyersdorff, O.: On the correspondence between arithmetic theories and propositional proof systems\u2013a survey. Math. Log. Q. 55(2), 116\u2013137 (2009)","journal-title":"Math. Log. Q."},{"key":"9609_CR9","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O.: The complexity of theorem proving in autoepistemic logic. In: Proceedings of 16th International Conference on Theory and Applications of Satisfiability Testing, volume 7962 of Lecture Notes in Computer Science, pp. 365\u2013376 (2013)","DOI":"10.1007\/978-3-642-39071-5_27"},{"key":"9609_CR10","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Log. Methods Comput. Sci. 15(1), 13:1\u201313:39 (2019)"},{"key":"9609_CR11","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Hardness characterisations and size-width lower bounds for QBF resolution. In: Proceedings of ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 209\u2013223. ACM (2020)","DOI":"10.1145\/3373718.3394793"},{"key":"9609_CR12","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Bonacina, I., Chew, L., Pich, J.: Frege systems for quantified Boolean logic. J. ACM 67(2), 9:1\u20139:36 (2020)","DOI":"10.1145\/3381881"},{"key":"9609_CR13","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L.: The complexity of theorem proving in circumscription and minimal entailment. In: Proceedings of International Joint Conference on Automated Reasoning (IJCAR), pp. 403\u2013417 (2014)","DOI":"10.1007\/978-3-319-08587-6_32"},{"key":"9609_CR14","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory 11(4), 26:1\u201326:42 (2019)","DOI":"10.1145\/3352155"},{"key":"9609_CR15","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. Log. Methods Comput. Sci. 13, 1\u201320 (2017)"},{"key":"9609_CR16","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not so simple. ACM Trans. Comput. Log. 19, 1:1\u20131:26 (2018)","DOI":"10.1145\/3157053"},{"key":"9609_CR17","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.jcss.2016.11.011","volume":"104","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Chew, L., Sreenivasaiah, K.: A game characterisation of tree-like Q-Resolution size. J. Comput. Syst. Sci. 104, 82\u2013101 (2019)","journal-title":"J. Comput. Syst. Sci."},{"issue":"18","key":"9609_CR18","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ipl.2013.06.002","volume":"113","author":"O Beyersdorff","year":"2013","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: A characterization of tree-like resolution size. Inf. Process. Lett. 113(18), 666\u2013671 (2013)","journal-title":"Inf. Process. Lett."},{"key":"9609_CR19","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: Parameterized complexity of DPLL search procedures. ACM Trans. Comput. Log. 14(3), 20:1\u201320:21 (2013)","DOI":"10.1145\/2499937.2499941"},{"key":"9609_CR20","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M., Razborov, A.: Parameterized bounded-depth Frege is not optimal. ACM Trans. Comput. Theory 4(3), 7:1\u20137:16 (2012)","DOI":"10.1145\/2355580.2355582"},{"key":"9609_CR21","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. ACM Trans. Comput. Theory 12(2), 10:1\u201310:27 (2020)","DOI":"10.1145\/3378665"},{"key":"9609_CR22","first-page":"1177","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","author":"O Beyersdorff","year":"2021","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pp. 1177\u20131221. IOS Press, Amsterdam (2021)"},{"key":"9609_CR23","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Kutz, O.: Proof complexity of non-classical logics. In: Bezhanishvili, N., Goranko, V. (eds.) Lectures on Logic and Computation\u2014ESSLLI 2010 \/ESSLLI 2011. Selected Lecture Notes, pp. 1\u201354. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31485-8_1"},{"issue":"7","key":"9609_CR24","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/s00153-011-0245-8","volume":"50","author":"O Beyersdorff","year":"2011","unstructured":"Beyersdorff, O., Meier, A., M\u00fcller, S., Thomas, M., Vollmer, H.: Proof complexity of propositional default logic. Arch. Math. Log. 50(7), 727\u2013742 (2011)","journal-title":"Arch. Math. Log."},{"key":"9609_CR25","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)"},{"key":"9609_CR26","unstructured":"Blake, A.: Canonical expressions in Boolean algebra. PhD thesis, University of Chicago (1937)"},{"issue":"5","key":"9609_CR27","doi-asserted-by":"publisher","first-page":"1462","DOI":"10.1137\/S0097539799352474","volume":"30","author":"ML Bonet","year":"2000","unstructured":"Bonet, M.L., Esteban, J.L., Galesi, N., Johannsen, J.: On the relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput. 30(5), 1462\u20131484 (2000)","journal-title":"SIAM J. Comput."},{"key":"9609_CR28","doi-asserted-by":"publisher","first-page":"916","DOI":"10.2307\/2273826","volume":"52","author":"SR Buss","year":"1987","unstructured":"Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Log. 52, 916\u2013927 (1987)","journal-title":"J. Symb. Log."},{"issue":"7","key":"9609_CR29","doi-asserted-by":"publisher","first-page":"906","DOI":"10.1016\/j.apal.2011.09.009","volume":"163","author":"SR Buss","year":"2012","unstructured":"Buss, S.R.: Towards NP-P via proof complexity and search. Ann. Pure Appl. Log. 163(7), 906\u2013917 (2012)","journal-title":"Ann. Pure Appl. Log."},{"key":"9609_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511676277","volume-title":"Logical Foundations of Proof Complexity","author":"SA Cook","year":"2010","unstructured":"Cook, S.A., Nguyen, P.: Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge (2010)"},{"issue":"1","key":"9609_CR31","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"key":"9609_CR32","doi-asserted-by":"crossref","unstructured":"Dantchev, S.S., Riis, S.: Tree resolution proofs of the weak pigeon-hole principle. In Proceedings of 16th Annual IEEE Conference on Computational Complexity, pp. 69\u201375 (2001)","DOI":"10.1109\/CCC.2001.933873"},{"key":"9609_CR33","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 210\u2013215 (1960)","journal-title":"J. ACM"},{"issue":"3","key":"9609_CR34","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1145\/377978.377987","volume":"2","author":"U Egly","year":"2001","unstructured":"Egly, U., Tompits, H.: Proof-complexity results for nonmonotonic reasoning. ACM Trans. Comput. Log. 2(3), 340\u2013387 (2001)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"9609_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","volume":"65","author":"P Enjalbert","year":"1989","unstructured":"Enjalbert, P., del Cerro, L.F.: Modal resolution in clausal form. Theor. Comput. Sci. 65(1), 1\u201333 (1989)","journal-title":"Theor. Comput. Sci."},{"key":"9609_CR36","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Modal proof theory. In: Handbook of Modal Logic, pp. 85\u2013138. Elsevier, Amsterdam (2007)","DOI":"10.1016\/S1570-2464(07)80005-X"},{"key":"9609_CR37","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods. Kluwer (1998)","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"9609_CR38","doi-asserted-by":"crossref","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985) . Comput. Sci. 39, 297\u2013308 (1985)","DOI":"10.1016\/0304-3975(85)90144-6"},{"issue":"3","key":"9609_CR39","doi-asserted-by":"publisher","first-page":"941","DOI":"10.2178\/jsl\/1191333849","volume":"72","author":"P Hrube\u0161","year":"2007","unstructured":"Hrube\u0161, P.: Lower bounds for modal logics. J. Symb. Log. 72(3), 941\u2013958 (2007)","journal-title":"J. Symb. Log."},{"issue":"2\u20133","key":"9609_CR40","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.apal.2008.09.013","volume":"157","author":"P Hrube\u0161","year":"2009","unstructured":"Hrube\u0161, P.: On lengths of proofs in non-classical logics. Ann. Pure Appl. Log. 157(2\u20133), 194\u2013205 (2009)","journal-title":"Ann. Pure Appl. Log."},{"key":"9609_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2016.01.004","volume":"234","author":"M Janota","year":"2016","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1\u201325 (2016)","journal-title":"Artif. Intell."},{"issue":"1\u20132","key":"9609_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2008.10.005","volume":"159","author":"E Je\u0159\u00e1bek","year":"2009","unstructured":"Je\u0159\u00e1bek, E.: Substitution Frege and extended Frege proof systems in non-classical logics. Ann. Pure Appl. Log. 159(1\u20132), 1\u201348 (2009)","journal-title":"Ann. Pure Appl. Log."},{"issue":"2","key":"9609_CR43","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"key":"9609_CR44","unstructured":"Kraj\u00ed\u010dek, J.: Proof complexity. In: Encyclopedia of Mathematics and Its Applications, vol. 170. Cambridge University Press (2019)"},{"key":"9609_CR45","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: Automated Deduction\u2014CADE 26\u201426th International Conference on Automated Deduction, pp. 371\u2013384 (2017)","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"9609_CR46","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-10575-8_9","volume-title":"Handbook of Model Checking","author":"J Marques-Silva","year":"2018","unstructured":"Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 247\u2013275. Springer, Berlin (2018)"},{"key":"9609_CR47","unstructured":"Montmirail, V.: Practical resolution of satisfiability testing for modal logics. (R\u00e9solution pratique du test de coh\u00e9rence en logiques modales), PhD thesis. Artois University, Arras, France (2018)"},{"issue":"3\u20134","key":"9609_CR48","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.jalgor.2007.04.001","volume":"62","author":"C Nalon","year":"2007","unstructured":"Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. J. Algorithms 62(3\u20134), 117\u2013134 (2007)","journal-title":"J. Algorithms"},{"key":"9609_CR49","doi-asserted-by":"crossref","unstructured":"Nalon, C., Dixon, C., Hustadt, U.: Modal resolution: proofs, layers, and refinements. ACM Trans. Comput. Log. 20(4), 23:1\u201323:38 (2019)","DOI":"10.1145\/3331448"},{"key":"9609_CR50","doi-asserted-by":"crossref","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: A modal-layered resolution calculus for K. I:n Automated Reasoning with Analytic Tableaux and Related Methods\u201424th International Conference, (TABLEAUX\u201915), pp. 185\u2013200 (2015)","DOI":"10.1007\/978-3-319-24312-2_13"},{"key":"9609_CR51","doi-asserted-by":"crossref","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: KSP: a resolution-based prover for multimodal K, abridged report. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI\u201917), pp. 4919\u20134923 (2017)","DOI":"10.24963\/ijcai.2017\/694"},{"key":"9609_CR52","doi-asserted-by":"crossref","unstructured":"Nalon, C., Pattinson, D.: A resolution-based calculus for preferential logics. In: Proceedings of International Joint Conference on Automated Reasoning (IJCAR), pp. 498\u2013515. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_33"},{"issue":"4","key":"9609_CR53","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1093\/logcom\/ext074","volume":"24","author":"C Nalon","year":"2014","unstructured":"Nalon, C., Zhang, L., Dixon, C., Hustadt, U.: A resolution-based calculus for coalition logic. J. Log. Comput. 24(4), 883\u2013917 (2014)","journal-title":"J. Log. Comput."},{"issue":"3","key":"9609_CR54","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2815493.2815497","volume":"2","author":"J Nordstr\u00f6m","year":"2015","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. SIGLOG News 2(3), 19\u201344 (2015)","journal-title":"SIGLOG News"},{"issue":"2","key":"9609_CR55","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"issue":"3","key":"9609_CR56","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symb. Log. 62(3), 981\u2013998 (1997)","journal-title":"J. Symb. Log."},{"key":"9609_CR57","unstructured":"Pudl\u00e1k, P., Impagliazzo, R.: A lower bound for DLL algorithms for SAT. In: Proceedings of 11th Symposium on Discrete Algorithms, pp. 128\u2013136 (2000)"},{"key":"9609_CR58","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"9609_CR59","first-page":"1223","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","author":"R Sebastiani","year":"2021","unstructured":"Sebastiani, R., Tacchella, A.: SAT techniques for modal and description logics. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pp. 1223\u20131266. IOS Press, Amsterdam (2021)"},{"issue":"4","key":"9609_CR60","doi-asserted-by":"publisher","first-page":"417","DOI":"10.2178\/bsl\/1203350879","volume":"13","author":"N Segerlind","year":"2007","unstructured":"Segerlind, N.: The complexity of propositional proofs. Bull. Symb. Log. 13(4), 417\u2013481 (2007)","journal-title":"Bull. Symb. Log."},{"key":"9609_CR61","unstructured":"Sigley, S.: Proof complexity of modal resolution systems. PhD thesis, University of Leeds, UK (2019)"},{"issue":"2","key":"9609_CR62","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1093\/logcom\/4.2.125","volume":"4","author":"H Wansing","year":"1994","unstructured":"Wansing, H.: Sequent calculi for normal modal propositional logics. J. Log. Comput. 4(2), 125\u2013142 (1994)","journal-title":"J. Log. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09609-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09609-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09609-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T22:30:46Z","timestamp":1725921046000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09609-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,13]]},"references-count":62,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["9609"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09609-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,10,13]]},"assertion":[{"value":"3 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 September 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 October 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}