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 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 procedure. KSAT is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system KRIS. The experimental results show that KSAT outperforms KRIS and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decision procedures, and provide partial evidence of a phase transition phenomenon for K(m)
Building decision procedures for modal logics from propositiional decision procedures - the case study of modal K(m)
Giunchiglia, Fausto;Sebastiani, Roberto
2000-01-01
Abstract
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 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 procedure. KSAT is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system KRIS. The experimental results show that KSAT outperforms KRIS and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decision procedures, and provide partial evidence of a phase transition phenomenon for K(m)I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
