ML Anthology

KSP: A Resolution-Based Prover for Multimodal K, Abridged Report

Cláudia Nalon, Ullrich Hustadt, Clare Dixon
IJCAI 2017 pp. 4919-4923
doi:10.24963/IJCAI.2017/694 /ijcai/2017/nalon2017ijcai-ksp/

Abstract

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.

PDF IJCAI Semantic Scholar

Cite

Text

Nalon et al. "KSP: A Resolution-Based Prover for Multimodal K, Abridged Report." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/694

Markdown

[Nalon et al. "KSP: A Resolution-Based Prover for Multimodal K, Abridged Report." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/nalon2017ijcai-ksp/) doi:10.24963/IJCAI.2017/694

BibTeX

@inproceedings{nalon2017ijcai-ksp,
  title     = {{KSP: A Resolution-Based Prover for Multimodal K, Abridged Report}},
  author    = {Nalon, Cláudia and Hustadt, Ullrich and Dixon, Clare},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2017},
  pages     = {4919-4923},
  doi       = {10.24963/IJCAI.2017/694},
  url       = {https://mlanthology.org/ijcai/2017/nalon2017ijcai-ksp/}
}