Modal Resolution: Proofs, Layers and Refinements
- Submitting institution
-
The University of Manchester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 173413113
- Type
- D - Journal article
- DOI
-
10.1145/3331448
- Title of journal
- ACM Transactions on Computational Logic
- Article number
- 23
- First page
- -
- 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)
-
A - Computer Science
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- "This paper describes the calculus for a theorem prover for the modal logic K which has been implemented as the prover KSP. KSP outperforms other modal provers on formulae with a high degree of nesting of the modal operators.
Based on TABLEAUX 2015 and IJCAR 2016 papers, it was nominated by the IJCAR PC chairs for IJCAI 2017''s Sister Conference Best Paper Track.
Led to Nalon co-organising the Dagsthul seminar 20061 with all co-authors attending, is used in Sigley''s PhD thesis (Leeds 2019), Montmirail''s 2018 PhD describes it ""state-of-the-art"" and is used for benchmarking e.g. Lagniez et al (IJCAI 2017)."
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
