SAT-Based Decision Procedures for Classical Modal Logics |
| |
Authors: | Enrico Giunchiglia Armando Tacchella Fausto Giunchiglia |
| |
Affiliation: | (1) DIST, V.le Causa 13, 16145 Genova, Italy;(2) DISA, Università di Trento, IRST, 38050 Povo, Trento, Italy |
| |
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 that 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. |
| |
Keywords: | SAT-based decision procedure modal logic |
本文献已被 SpringerLink 等数据库收录! |
|