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.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.