Non-iterative Modal Resolution Calculi

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.