Cláudia Nalon, Ullrich Hustadt, and Clare Dixon (2017): ``KSP: A Resolution-Based Prover for Multimodal K (Abridged Report).'' In C. Sierra, editors, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017) [Melbourne, Australia, 19-25 August 2017], pp. 4919-4923,
Abstract, BibTeX. PDF

In this paper, we briefly describe an implementation of a hyper-resolution-based calculus for the propositional basic multimodal logic, Kn. The prover, KSP, is designed to support experimentation with different combinations of refinements for its basic calculus. The prover allows for both local and global reasoning. We present an experimental evaluation that compares KSP with a range of existing reasoners for Kn.

Maintained by Ullrich Hustadt,, last updated Monday, 02-Apr-2018 21:11:22 BST © 2018 by Ullrich Hustadt.