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 proceduresI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
