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).

[img] Text
layered-ksp-tocl.pdf - Accepted Version

Download (836kB) | Preview


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
Depositing User: Symplectic Admin
Date Deposited: 20 Jun 2019 07:48
Last Modified: 11 Jun 2022 04:11
DOI: 10.1145/3331448
Open Access URL:
Related URLs: