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 a modular implementation for these logics. For some of the logics we deal with, we are not aware of any other implementation. For the others, we define a testing methodology which generalizes the 3CNFK methodology by Giunchiglia and Sebastiani. 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, Enrico; Tacchella, Armando; Giunchiglia, Fausto. - ELETTRONICO. - (2005).
SAT-Based Decision Procedures for Classical Modal Logics
Giunchiglia, Fausto
2005-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 a modular implementation for these logics. For some of the logics we deal with, we are not aware of any other implementation. For the others, we define a testing methodology which generalizes the 3CNFK methodology by Giunchiglia and Sebastiani. The experimental evaluation shows that our decision procedures perform better than or as well as other state-of-the-art decision procedures.File | Dimensione | Formato | |
---|---|---|---|
001.pdf
accesso aperto
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
792.39 kB
Formato
Adobe PDF
|
792.39 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione