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,
ijcai.org.
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,
U.Hustadt@liverppol.ac.uk,
last updated
© 2018 by Ullrich Hustadt.