K_SP: A Resolution-Based Prover for Multimodal K

Nalon, Claudia, Hustadt, Ullrich ORCID: 0000-0002-0455-0267 and Dixon, Clare ORCID: 0000-0002-4610-9533 (2016) K_SP: A Resolution-Based Prover for Multimodal K. In: International Joint Conference on Automated Reasoning, 2016-6-27 - 2016-7-2, Coimbra, Portugal.

Text main.pdf - Unspecified Access to this file is embargoed until Unspecified. Download (453kB)

Abstract

In this paper, we describe an implementation of a hyperresolution- based calculus for the propositional basic multimodal logic, Kn. The prover was designed to support experimentation with different combinations of refinements for its basic calculus: it is primarily based on the set of support strategy, which can then be combined with other refinements, simplification techniques and different choices for the underlying normal form and clause selection. The prover allows for both local and global reasoning. We show experimental results for different combinations of strategies and comparison with existing tools.

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	14 Apr 2016 13:22
Last Modified:	14 Oct 2023 09:35
DOI:	10.1007/978-3-319-40229-1_28
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3000494