@inproceedings{267b141c26a748b2a696d85143eaa017,
title = "Non-iterative Modal Resolution Calculi",
abstract = "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.",
keywords = "Automated Reasoning, Modal Logics, Resolution",
author = "Dirk Pattinson and Cl{\'a}udia Nalon",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.; 12th International Joint Conference on Automated Reasoning, IJCAR 2024 ; Conference date: 03-07-2024 Through 06-07-2024",
year = "2024",
doi = "10.1007/978-3-031-63501-4_6",
language = "English",
isbn = "9783031635007",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "97--113",
editor = "Christoph Benzm{\"u}ller and Heule, {Marijn J. H.} and Schmidt, {Renate A.}",
booktitle = "Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings",
address = "Germany",
}