KSP A Resolution-Based Theorem Prover for K_n : Architecture, Refinements, Strategies and Experiments

Nalon, C, Hustadt, U ORCID: 0000-0002-0455-0267 and Dixon, C (2020) KSP A Resolution-Based Theorem Prover for K_n : Architecture, Refinements, Strategies and Experiments. Journal of Automated Reasoning, 64 (3). pp. 461-484.

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

Text jar-2017.pdf - Author Accepted Manuscript Download (537kB)

Abstract

In this paper we describe the implementation of KSP, a resolution-based prover for the basic multimodal logic Kn. The prover implements a resolution-based calculus for both local and global reasoning. The user can choose different normal forms, refinements of the basic resolution calculus, and strategies. We describe these options in detail and discuss their implications. We provide experiments comparing some of these options and comparing the prover with other provers for this logic.

Item Type:	Article
Uncontrolled Keywords:	Modal logics, Theorem proving, Resolution method
Depositing User:	Symplectic Admin
Date Deposited:	16 Jan 2019 10:55
Last Modified:	19 Jan 2023 01:06
DOI:	10.1007/s10817-018-09503-x
Open Access URL:	https://link.springer.com/article/10.1007/s10817-0...
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3031352