Building decision procedures for modal logics from propositional decision procedures: The case study of modal K(m)

The goal of this paper is to propose a new technique for developing decisio n procedures for propositional modal logics. The basic idea is that proposi tional modal decision procedures should be developed on top of propositiona l decision procedures. As a case study, we consider satisfiability in modal K(m), that is modal K with m modalities, and develop an algorithm, called KSAT, on top of an implementation of the Davis-Putnam-Longemann-Loveland pr ocedure. KSAT is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system KRIS. The exp erimental results show that KSAT outperforms KRIS and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decis ion procedures, and provide partial evidence of a phase transition phenomen on for K(m). (C) 2000 Academic Press.