Modal Resolution: Proofs, Layers and Refinements
- Submitting institution
-
The University of Liverpool
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 12175
- Type
- D - Journal article
- DOI
-
10.1145/3331448
- Title of journal
- ACM Transactions on Computational Logic
- Article number
- 23
- First page
- 1
- Volume
- 20
- Issue
- 4
- ISSN
- 1529-3785
- Open access status
- Compliant
- Month of publication
- August
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This article introduces and investigates a resolution calculus for modal logic. It combines and extends two conference papers: "A Modal-Layered Resolution Calculus for K" (TABLEAUX'15) introduces the underlying calculus and "KSP: A resolution-based prover for multimodal K" (IJCAR'16) gives the details of the prover. The second paper was invited to the Sister Conference Best Paper Track at IJCAI'17 and published as "KSP: A resolution-based prover for multimodal K. Abridged Report". The prover outperforms all other modal logic provers on formulae of large modal depth. The prover has been used, for example, to support benchmarking in Lagniez et al (IJCAI'17).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -