Nalon, Claudia, Hustadt, Ullrich ORCID: 0000-0002-0455-0267 and Dixon, CL ORCID: 0000-0002-4610-9533
(2020)
A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments.
Journal of Automated Reasoning, 64 (3).
pp. 461-484.
This is the latest version of this item.
Text
jar-2017.pdf - Author Accepted Manuscript Download (537kB) |
|
Text
Nalon2018_Article_AResolution-BasedTheoremProver.pdf - Published version Download (1MB) |
Abstract
In this paper we describe the implementation of , 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 |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3031374 |
Available Versions of this Item
-
KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments. (deposited 23 Nov 2018 10:04)
-
KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments. (deposited 29 Nov 2018 08:57)
- A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments. (deposited 16 Jan 2019 10:55) [Currently Displayed]
-
KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments. (deposited 29 Nov 2018 08:57)