The goal of this paper is to propose 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
Building Decision Procedures for Modal Logics from Propositional Decision Procedures - The Case Study of Modal K
Giunchiglia, Fausto;Sebastiani, Roberto
1996-01-01
Abstract
The goal of this paper is to propose 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 patternI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
