{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:56:20Z","timestamp":1781884580545,"version":"3.54.5"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We establish a systematic correspondence between sequent and resolution calculi for a broad class of modal logics. Our main result is that soundness and completeness transfer from sequent to resolution calculi as long as\u00a0cut and weakening are admissible. We first construct generative calculi\u00a0that essentially import modal rules to a resolution setting, and\u00a0then show how soundness and completeness transfer to absorptive calculi, where modal rules are translated into generalised resolution rules. We discuss resolution calculi that establish validity,\u00a0and then introduce local clauses to generate calculi for inconsistency. Finally, for modal rules of a certain shape, we show how\u00a0to construct layered resolution calculi, a technique that has so\u00a0far only been established for the modal logic K. Our work directly yields new sound and complete resolution calculi, and layered resolution calculi, for a large number of modal logics.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_20","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:34Z","timestamp":1753789654000},"page":"361-380","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From Modal Sequent Calculi to\u00a0Modal Resolution"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5832-6666","authenticated-orcid":false,"given":"Dirk","family":"Pattinson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9792-5346","authenticated-orcid":false,"given":"Cl\u00e1udia","family":"Nalon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sourabh","family":"Peruri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2001)","DOI":"10.1017\/CBO9781107050884"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Chellas, B.: Modal Logic. Cambridge (1980)","DOI":"10.1017\/CBO9780511621192"},{"key":"20_CR3","volume-title":"A New Introduction to Modal Logic","author":"MJ Cresswell","year":"1996","unstructured":"Cresswell, M.J., Hughes, G.E.: A New Introduction to Modal Logic. Routledge, New York (1996)"},{"key":"20_CR4","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"2003","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.: Reasoning About Knowledge. MIT Press, Cambridge (2003)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-25927-5_7","volume-title":"Deontic Logic in Computer Science","author":"L Goble","year":"2004","unstructured":"Goble, L.: A proposal for dealing with deontic dilemmas. In: Lomuscio, A., Nute, D. (eds.) DEON 2004. LNCS (LNAI), vol. 3065, pp. 74\u2013113. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25927-5_7"},{"key":"20_CR6","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, pp. 297\u2013396. Kluwer (1999)","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Greco, G., Kurz, A., Palmigiano, A.: Dynamic sequent calculus for the logic of epistemic actions and knowledge. In: Galatos, N., Kurz, A., Tsinakis, C. (eds.) Proceedings of TACL 2013. EPiC Series in Computing, vol. 25, pp. 85\u201387. EasyChair (2013)","DOI":"10.29007\/mwpp"},{"issue":"2","key":"20_CR8","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1305\/ndjfl\/1093635420","volume":"31","author":"J Hawthorn","year":"1990","unstructured":"Hawthorn, J.: Natural deduction in normal modal logic. Notre Dame J. Formal Log. 31(2), 263\u2013273 (1990)","journal-title":"Notre Dame J. Formal Log."},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1006\/game.1999.0788","volume":"35","author":"A Heifetz","year":"2001","unstructured":"Heifetz, A., Mongin, P.: Probabilistic logic for type spaces. Games Econom. Behav. 35, 31\u201353 (2001)","journal-title":"Games Econom. Behav."},{"issue":"3","key":"20_CR10","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-009-9153-6","volume":"44","author":"O Hermant","year":"2010","unstructured":"Hermant, O.: Resolution is cut-free. J. Autom. Reason. 44(3), 245\u2013276 (2010)","journal-title":"J. Autom. Reason."},{"key":"20_CR11","unstructured":"Kupke, C., Pattinson, D.: On modal logics of linear inequalities. In: Beklemishev, L.D., Goranko, V., Shehtman, V.B. (eds.) Proceedings of AiML 2010, pp. 235\u2013255. College Publications (2010)"},{"issue":"2","key":"20_CR12","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s11229-006-9143-8","volume":"155","author":"H Leitgeb","year":"2007","unstructured":"Leitgeb, H., Segerberg, K.: Dynamic doxastic logic: why, how, and where to? Synthese 155(2), 167\u2013190 (2007)","journal-title":"Synthese"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Mints, G.: Gentzen-type systems and resolution rules. Part I. Propositional logic. In: COLOG-88: Proceedings of the International Conference on Computer Logic, pp. 198\u2013231. Springer (1990)","DOI":"10.1007\/3-540-52335-9_55"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-94-017-2798-3_2","volume-title":"Proof Theory of Modal Logic","author":"G Mints","year":"1996","unstructured":"Mints, G., Orevkov, V., Tammet, T.: Transfer of sequent calculus strategies to resolution for S4. In: Wansing, H. (ed.) Proof Theory of Modal Logic, pp. 17\u201331. Springer, Dordrecht (1996)"},{"key":"20_CR15","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"},{"issue":"3","key":"20_CR16","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s10817-018-09503-x","volume":"64","author":"C Nalon","year":"2020","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: KSP: architecture, refinements, strategies and experiments. J. Autom. Reason. 64(3), 461\u2013484 (2020)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"20_CR17","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."},{"key":"20_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-8966-5","volume-title":"Topics in Conditional Logic","author":"D Nute","year":"1980","unstructured":"Nute, D.: Topics in Conditional Logic. Reidel, Boston (1980)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/BFb0012852","volume-title":"9th International Conference on Automated Deduction","author":"HJ Ohlbach","year":"1988","unstructured":"Ohlbach, H.J.: A resolution calculus for modal logics. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 500\u2013516. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/BFb0012852"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Olivetti, N., Pozzato, G.L., Schwind, C.: A sequent calculus and a theorem prover for standard conditional logics. ACM Trans. Comput. Log. 8(4) (2007)","DOI":"10.1145\/1276920.1276924"},{"issue":"1","key":"20_CR21","doi-asserted-by":"publisher","first-page":"139","DOI":"10.12775\/LLP.2020.018","volume":"30","author":"E Orlandelli","year":"2020","unstructured":"Orlandelli, E.: Sequent calculi and interpolation for non-normal modal and deontic logics. Logic Log. Philos. 30(1), 139\u2013183 (2020)","journal-title":"Logic Log. Philos."},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Pattinson, D., Schr\u00f6der, L.: Generic modal cut elimination applied to conditional logics. In: Giese, M., Waaler, A. (eds.) Proceedings of Tableaux 2009. Lecture Notes in Artificial Intelligence, vol. 5607. Springer (2009)","DOI":"10.1007\/978-3-642-02716-1_21"},{"key":"20_CR23","doi-asserted-by":"publisher","first-page":"1447","DOI":"10.1016\/j.ic.2009.11.008","volume":"208","author":"D Pattinson","year":"2010","unstructured":"Pattinson, D., Schr\u00f6der, L.: Cut elimination in coalgebraic logics. Inf. Comput. 208, 1447\u20131468 (2010)","journal-title":"Inf. Comput."},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Pattinson, D., Nalon, C.: Non-iterative modal resolution calculi. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) Proceedings of IJCAR 2024. Lecture Notes in Computer Science, vol. 14740, pp. 97\u2013113. Springer (2024)","DOI":"10.1007\/978-3-031-63501-4_6"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Pattinson, D., Nalon, C., Olivetti, N.: Resolution-based calculi for non-normal modal logics. In: Ramanayake, R., Urban, J. (eds.) Proceedings of Tableaux 2023 (2023)","DOI":"10.1007\/978-3-031-43513-3_18"},{"issue":"1","key":"20_CR26","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1093\/logcom\/12.1.149","volume":"12","author":"M Pauly","year":"2002","unstructured":"Pauly, M.: A modal logic for coalitional power in games. J. Logic Comput. 12(1), 149\u2013166 (2002)","journal-title":"J. Logic Comput."},{"issue":"8","key":"20_CR27","doi-asserted-by":"publisher","first-page":"1061","DOI":"10.1017\/S0960129518000476","volume":"29","author":"G Reis","year":"2019","unstructured":"Reis, G., Paleo, B.W.: Complexity of translations from resolution to sequent calculus. Math. Struct. Comput. Sci. 29(8), 1061\u20131091 (2019)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"20_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-021-09609-9","volume":"66","author":"S Sigley","year":"2022","unstructured":"Sigley, S., Beyersdorff, O.: Proof complexity of modal resolution. J. Autom. Reason. 66(1), 1\u201341 (2022)","journal-title":"J. Autom. Reason."},{"key":"20_CR29","unstructured":"Stewart, C., Stouppa, P.: A systematic proof theory for several modal logics. In: Schmidt, R.A., Pratt-Hartmann, I., Reynolds, M., Wansing, H. (eds.) Proceedings of AIML 2004, pp. 309\u2013333. King\u2019s College Publications (2004)"},{"key":"20_CR30","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1613\/jair.813","volume":"14","author":"U Straccia","year":"2001","unstructured":"Straccia, U.: Reasoning within fuzzy description logics. J. Artif. Intell. Res. (JAIR) 14, 137\u2013166 (2001)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"20_CR31","unstructured":"Sutcliff, G.: Proceedings of the 12th IJCAR ATP System Competition (CASC-J1j) (2024). https:\/\/www.tptp.org\/CASC\/J12\/"},{"key":"20_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/3-540-63385-5_33","volume-title":"Computational Logic and Proof Theory","author":"T Tammet","year":"1997","unstructured":"Tammet, T.: Resolution, inverse method and the sequent calculus. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol. 1289, pp. 65\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63385-5_33"},{"key":"20_CR33","unstructured":"Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Number\u00a043 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1996)"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic: Volume 8, pp. 61\u2013145. Springer (2002)","DOI":"10.1007\/978-94-010-0387-2_2"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:26:12Z","timestamp":1781882772000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}