K<inf>S</inf>P: A resolution-based prover for multimodal K abridged report

Nalon, C, Hustadt, U ORCID: 0000-0002-0455-0267 and Dixon, C ORCID: 0000-0002-4610-9533 (2017) K<inf>S</inf>P: A resolution-based prover for multimodal K abridged report. In: Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017-8-19 - 2017-8-26.

Access the full-text of this item by clicking on the Open Access link.

Official URL: https://doi.org/10.24963/ijcai.2017/694

Abstract

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

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	25 Jan 2018 15:04
Last Modified:	07 Dec 2024 11:06
DOI:	10.24963/ijcai.2017/694
Open Access URL:	https://doi.org/10.24963/ijcai.2017/694
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3016846