In the last two decades, modal and description logics have been applied to numerous areas of computer science, including artificial intelligence, formal verification, database theory, and distributed computing. For this reason, the problem of automated reasoning in modal and description logics has been throughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic Km, and of its notational variant, the description logic ALC. Although simple in structure, Km/ALC is computationally very hard to reason on, its satisfiability being PSPACE-complete. In this paper we explore the idea of encoding Km/ALC-satisfiability into SAT, so that to be handled by state-of-the-art SAT tools.We propose an efficient encoding, and we test it on an extensive set of benchmarks, comparing the approach with the main state-of-the-art tools available. Although the encoding is necessarily worst-case exponential, from our experiments we notice that, in practice, this approach can handle most or all the problems which are at the reach of the other approaches, with performances which are comparable with, or even better than, those of the current state-of-the-art tools.

Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC / Sebastiani, Roberto; Vescovi, Michele. - ELETTRONICO. - (2006), pp. 1-23.

Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC

Sebastiani, Roberto;Vescovi, Michele
2006-01-01

Abstract

In the last two decades, modal and description logics have been applied to numerous areas of computer science, including artificial intelligence, formal verification, database theory, and distributed computing. For this reason, the problem of automated reasoning in modal and description logics has been throughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic Km, and of its notational variant, the description logic ALC. Although simple in structure, Km/ALC is computationally very hard to reason on, its satisfiability being PSPACE-complete. In this paper we explore the idea of encoding Km/ALC-satisfiability into SAT, so that to be handled by state-of-the-art SAT tools.We propose an efficient encoding, and we test it on an extensive set of benchmarks, comparing the approach with the main state-of-the-art tools available. Although the encoding is necessarily worst-case exponential, from our experiments we notice that, in practice, this approach can handle most or all the problems which are at the reach of the other approaches, with performances which are comparable with, or even better than, those of the current state-of-the-art tools.
2006
Trento
Università degli Studi di Trento - Dipartimento di Informatica e Telecomunicazioni
Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC / Sebastiani, Roberto; Vescovi, Michele. - ELETTRONICO. - (2006), pp. 1-23.
Sebastiani, Roberto; Vescovi, Michele
File in questo prodotto:
File Dimensione Formato  
033.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 452.58 kB
Formato Adobe PDF
452.58 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/358096
 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