Modal Resolution: Proofs, Layers and Refinements

Nalon, C, Dixon, Clare ORCID: 0000-0002-4610-9533 and Hustadt, U ORCID: 0000-0002-0455-0267 (2019) Modal Resolution: Proofs, Layers and Refinements. ACM Transactions on Computational Logic, 20 (4). pp. 1-38.

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

Text
layered-ksp-tocl.pdf - Author Accepted Manuscript
Download (836kB) | Preview

Official URL: https://dl.acm.org/doi/10.1145/3331448

Abstract

Resolution-based provers for multimodal normal logics require pruning of the search space for a proof in order to ameliorate the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution calculus for the basic multimodal logic, which divides the clause set according to the modal level at which clauses occur in order to reduce the number of possible inferences. We show that the calculus is complete for the logics being considered. We also show that the calculus can be combined with other strategies. In particular, we discuss the completeness of combining modal layering with negative and ordered resolution and provide experimental results comparing the different refinements.

Item Type:	Article
Uncontrolled Keywords:	Normal modal logics, resolution method, proof strategies
Depositing User:	Symplectic Admin
Date Deposited:	20 Jun 2019 07:48
Last Modified:	19 Jan 2023 00:40
DOI:	10.1145/3331448
Open Access URL:	https://doi.org/10.1145/3331448
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3045580