The goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we describe an algorithm, based on an implementation of the Davis-Putnam-Longemann-Loveland procedure, which tests satisfiability in modal K. The algorithm is compared with a tableau based decision procedure. The experimental results show that our algorithm outperforms this system. The testing is performed following a newly developed methodology which, among other things, allows us to classify problems according to an easy to hard pattern.
CITATION STYLE
Giunchiglia, F., & Sebastiani, R. (1996). Building decision procedures for modal logics from propositional decision procedures — The case study of modal K. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1104, pp. 583–597). Springer Verlag. https://doi.org/10.1007/3-540-61511-3_115
Mendeley helps you to discover research relevant for your work.