We propose a novel approach to axiom pinpointing based on a reduction to the SAT task of minimal unsatisfiable subformula enumeration, allowing highly optimized algorithms and data structures developed for SAT solving in the last two decades to be used in this problem. Exploiting the specific properties of axiom pinpointing, we apply further optimizations resulting in considerable runtime improvements of several orders of magnitude. Our ideas are implemented in SATPIN, a system capable of performing axiom pinpointing in large biomedical ontologies faster than other existing tools. While our paper focuses on a slight extension of EL, the presented approach directly generalizes to all ontology languages for which consequence-based reasoning methods are available.

Manthey, N., Peñaloza, R., Rudolph, S. (2016). Efficient axiom pinpointing in EL using SAT Technology. In Proceedings of the 2016 International Workshop on Description Logics (DL'16). CEUR-WS.

Efficient axiom pinpointing in EL using SAT Technology

Peñaloza, R
;
2016

Abstract

We propose a novel approach to axiom pinpointing based on a reduction to the SAT task of minimal unsatisfiable subformula enumeration, allowing highly optimized algorithms and data structures developed for SAT solving in the last two decades to be used in this problem. Exploiting the specific properties of axiom pinpointing, we apply further optimizations resulting in considerable runtime improvements of several orders of magnitude. Our ideas are implemented in SATPIN, a system capable of performing axiom pinpointing in large biomedical ontologies faster than other existing tools. While our paper focuses on a slight extension of EL, the presented approach directly generalizes to all ontology languages for which consequence-based reasoning methods are available.
paper
SAT, description logics, axiom pinpointing
English
International Workshop on Description Logics (DL 2016)
2016
Lenzerini, M; Peñaloza, R
Proceedings of the 2016 International Workshop on Description Logics (DL'16)
2016
1577
open
Manthey, N., Peñaloza, R., Rudolph, S. (2016). Efficient axiom pinpointing in EL using SAT Technology. In Proceedings of the 2016 International Workshop on Description Logics (DL'16). CEUR-WS.
File in questo prodotto:
File Dimensione Formato  
DL.pdf

accesso aperto

Tipologia di allegato: Submitted Version (Pre-print)
Dimensione 393.14 kB
Formato Adobe PDF
393.14 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/10281/256919
Citazioni
  • Scopus 8
  • ???jsp.display-item.citation.isi??? ND
Social impact