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)
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/1727
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact