C. Nalon, U. Hustadt, and C. Dixon (2015): ``A Modal-Layered Resolution Calculus for K.'' In H. de Nivelle, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015) [Wroclaw, Poland, 20--24 September 2015], pp. 181-196. LNAI 9323, Springer International Publishing Switzerland 2015.
Abstract, BibTeX. PDF (© Springer).

Resolution-based provers for multimodal normal logics require pruning of the search space for a proof in order to deal with the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution calculus for the basic multimodal logic, which divides the clause set according to the modal depth at which clauses occur. We show that the calculus is complete for the logics being considered. We also show that the calculus can be combined with other strategies. In particular, we discuss the completeness of combining modal layering and negative resolution. In addition, we present an incompleteness result for modal layering together with ordered resolution.