{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:52:03Z","timestamp":1781927523368,"version":"3.54.5"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031635007","type":"print"},{"value":"9783031635014","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T00:00:00Z","timestamp":1719878400000},"content-version":"vor","delay-in-days":183,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Non-monotonic modal logics are typically interpreted over neighbourhood frames. For unary operators, this is just a set of worlds, together with an endofunction on predicates (subsets of worlds). It is known that all systems of not necessarily monotonic modal logics that are axiomatised by formulae of modal rank at most one (non-iterative modal logics) are Kripke-complete over neighbourhood semantics. In this paper, we give a uniform construction to obtain complete resolution calculi for all non-iterative logics. We show completeness for generative calculi (where new clauses with new literals are added to the clause set) by means of a canonical model construction. We then define absorptive calculi (where new clauses are generated by generalised resolution rules) and establish completeness by translating between generative and absorptive calculi. Instances of our construction re-prove completeness for already known calculi, but also give rise to a number of previously unknown complete calculi.<\/jats:p>","DOI":"10.1007\/978-3-031-63501-4_6","type":"book-chapter","created":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:00Z","timestamp":1719824520000},"page":"97-113","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Non-iterative Modal Resolution Calculi"],"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"}]}],"member":"297","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-16780-3_89","volume-title":"8th International Conference on Automated Deduction","author":"M Abadi","year":"1986","unstructured":"Abadi, M., Manna, Z.: Modal theorem proving. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 172\u2013189. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16780-3_89"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-48660-7_13","volume-title":"Automated Deduction \u2014 CADE-16","author":"C Areces","year":"1999","unstructured":"Areces, C., de Nivelle, H., de Rijke, M.: Prefixed resolution: a resolution method for modal and description logics. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 187\u2013201. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_13"},{"issue":"2","key":"6_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0020-0190(88)90169-X","volume":"28","author":"Y Auffray","year":"1988","unstructured":"Auffray, Y.: Linear strategy for propositional modal resolution. Inf. Process. Lett. 28(2), 87\u201392 (1988)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"6_CR4","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BF00881838","volume":"10","author":"A Avron","year":"1993","unstructured":"Avron, A.: Gentzen-type systems, resolution and tableaux. J. Autom. Reason. 10(2), 265\u2013281 (1993)","journal-title":"J. Autom. Reason."},{"key":"6_CR5","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"6_CR6","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":"6_CR7","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/BF03037397","volume":"5","author":"M-C Chan","year":"1987","unstructured":"Chan, M.-C.: The recursive resolution method for modal logic. N. Gener. Comput. 5, 155\u2013183 (1987)","journal-title":"N. Gener. Comput."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Chellas, B.: Modal Logic. Cambridge (1980)","DOI":"10.1017\/CBO9780511621192"},{"issue":"2","key":"6_CR9","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0020-0190(82)90085-0","volume":"14","author":"LF del Cerro","year":"1982","unstructured":"del Cerro, L.F.: A simple deduction method for modal logic. Inf. Process. Lett. 14(2), 49\u201351 (1982)","journal-title":"Inf. Process. Lett."},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/10720084_5","volume-title":"Frontiers of Combining Systems","author":"G Dowek","year":"2000","unstructured":"Dowek, G.: Axioms vs. rewrite rules: from completeness to cut elimination. In: Kirchner, H., Ringeissen, C. (eds.) FroCoS 2000. LNCS (LNAI), vol. 1794, pp. 62\u201372. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10720084_5"},{"key":"6_CR11","first-page":"1","volume":"2","author":"D Elgesem","year":"1997","unstructured":"Elgesem, D.: The modal logic of agency. Nord. J. Philos. Log. 2, 1\u201346 (1997)","journal-title":"Nord. J. Philos. Log."},{"key":"6_CR12","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. Theoret. Comput. Sci. 65, 1\u201333 (1989)","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"6_CR13","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1305\/ndjfl\/1093890715","volume":"13","author":"K Fine","year":"1972","unstructured":"Fine, K.: In so many possible worlds. Notre Dame J. Formal Logic 13(4), 516\u2013520 (1972)","journal-title":"Notre Dame J. Formal Logic"},{"key":"6_CR14","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."},{"key":"6_CR15","unstructured":"Lee, R.C.T.: A completeness theorem and computer program for finding theorems derivable from given axioms. Ph.D. thesis, Berkeley (1967)"},{"issue":"4","key":"6_CR16","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/BF00257488","volume":"3","author":"D Lewis","year":"1974","unstructured":"Lewis, D.: Intensional logics without interative axioms. J. Philos. Log. 3(4), 457\u2013466 (1974)","journal-title":"J. Philos. Log."},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","volume-title":"COLOG-88","author":"G Mints","year":"1990","unstructured":"Mints, G.: Gentzen-type systems and resolution rules part I propositional logic. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 198\u2013231. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_55"},{"key":"6_CR18","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, 117\u2013134 (2007)","journal-title":"J. Algorithms"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Olivetti, N., Pozzato, G.L., Schwind, C.B.: A sequent calculus and a theorem prover for standard conditional logics. ACM Trans. Comput. Logic 8(4) (2007)","DOI":"10.1145\/1276920.1276924"},{"key":"6_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-031-43513-3_18","volume-title":"TABLEAUX 2023","author":"D Pattinson","year":"2023","unstructured":"Pattinson, D., Olivetti, N., Nalon, C.: Resolution calculi for non-normal modal logics. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS, vol. 14278, pp. 322\u2013341. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_18"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-02716-1_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D Pattinson","year":"2009","unstructured":"Pattinson, D., Schr\u00f6der, L.: Generic modal cut elimination applied to conditional logics. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 280\u2013294. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_21"},{"issue":"1","key":"6_CR22","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."},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11690634_11","volume-title":"Foundations of Software Science and Computation Structures","author":"L Schr\u00f6der","year":"2006","unstructured":"Schr\u00f6der, L.: A finite model construction for coalgebraic modal logic. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 157\u2013171. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11690634_11"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jal.2010.11.001","volume":"9","author":"C Stra\u00dfer","year":"2011","unstructured":"Stra\u00dfer, C.: A deontic logic framework allowing for factual detachment. J. Appl. Log. 9, 61\u201380 (2011)","journal-title":"J. Appl. Log."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63501-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:45Z","timestamp":1719824565000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63501-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031635007","9783031635014"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63501-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 July 2024","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":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}