We present a set of SAT-based decision procedures for various classical modal logics. By SAT-based, we mean built on top of a SAT solver. We show how the SAT-based approach allows for an efficient and modular implementation for these logics. For some of the logics we deal with, we are not aware of any other implementation, nor of any existing reduction into first order logic. For the others, we define a testing methodology which generalizes the 3CNF_K methodology by Giunchiglia and Sebastiani, and which is suitable for testing systems for classical modal logics. The experimental evaluation shows that our decision procedures perform better than or as well as other state-of-the-art decision procedures

SAT-Based Decision Procedures for Classical Modal Logics

Giunchiglia, Fausto;
2000-01-01

Abstract

We present a set of SAT-based decision procedures for various classical modal logics. By SAT-based, we mean built on top of a SAT solver. We show how the SAT-based approach allows for an efficient and modular implementation for these logics. For some of the logics we deal with, we are not aware of any other implementation, nor of any existing reduction into first order logic. For the others, we define a testing methodology which generalizes the 3CNF_K methodology by Giunchiglia and Sebastiani, and which is suitable for testing systems for classical modal logics. The experimental evaluation shows that our decision procedures perform better than or as well as other state-of-the-art decision procedures
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/1761
 Attenzione

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

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