Efficient Local Reductions to Basic Modal Logic
Open Access
- 5 July 2021
- book chapter
- Published by Springer Nature
- p. 76-92
Abstract
We present novel reductions of the propositional modal logics "Image missing" , "Image missing" , "Image missing" , "Image missing" and "Image missing" to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover "Image missing" to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover "Image missing" performs well when compared with a specialised resolution calculus for these logics and with the b̆uilt-in reductions of the first-order prover SPASS.Keywords
This publication has 24 references indexed in Scilit:
- Prefixed tableaus and nested sequentsAnnals of Pure and Applied Logic, 2012
- Multimodal and intuitionistic logics in simple type theoryLogic Journal of the IGPL, 2010
- The axiomatic translation principle for modal logicACM Transactions on Computational Logic, 2007
- Clausal resolution for normal modal logicsJournal of Algorithms, 2007
- 4 Computational modal logic2007
- BDD-based decision procedures for the modal logic K ★Journal of Applied Non-Classical Logics, 2006
- Reducing Modal Consequence RelationsJournal of Logic and Computation, 2001
- Labelled propositional modal logics: theory and practiceJournal of Logic and Computation, 1997
- A guide to completeness and complexity for modal logics of knowledge and beliefArtificial Intelligence, 1992
- Decidability results in non-classical logics: Part IAnnals of Mathematical Logic, 1975