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. - (1999).

SAT-Based Decision Procedures for Classical Modal Logics

Giunchiglia, Fausto
1999-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.
1999
Trento, Italia
Università degli Studi di Trento. DEPARTMENT OF INFORMATION AND COMMUNICATION TECHNOLOGY
SAT-Based Decision Procedures for Classical Modal Logics / Giunchiglia, Enrico; Tacchella, Armando; Giunchiglia, Fausto. - ELETTRONICO. - (1999).
Giunchiglia, Enrico; Tacchella, Armando; Giunchiglia, Fausto
File in questo prodotto:
File Dimensione Formato  
23.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 577.35 kB
Formato Adobe PDF
577.35 kB Adobe PDF Visualizza/Apri

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/11572/358347
 Attenzione

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

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