Cláudia Nalon, Ullrich Hustadt, and Clare Dixon (2016): ``K_SP: A Resolution-Based Prover for Multimodal K.'' In N. Olivetti and A. Tiwari, editors, Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016) [Coimbra, Portugal, 27 June-2 July 2016], pp. 406-415. LNAI 9706, Springer, 2016.
Abstract, BibTeX. PDF (© Springer).

In this paper, we describe an implementation of a hyper-resolution-based calculus for the propositional basic multimodal logic K(n). The prover was designed to support experimentation with different combinations of refinements for its basic calculus: it is primarily based on the set of support strategy, which can then be combined with other refinements, simplification techniques and different choices for the underlying normal form and clause selection. The prover allows for both local and global reasoning. We show experimental results for different combinations of strategies and comparison with existing tools.