Efficient Axiom Pinpointing in EL using SAT Technology

Norbert MantheyNorbert Manthey, Rafael PeñalozaRafael Peñaloza, Sebastian RudolphSebastian Rudolph

Download

Norbert Manthey, Rafael Peñaloza, Sebastian Rudolph
Efficient Axiom Pinpointing in EL using SAT Technology
In Maurizio Lenzerini, Rafael Peñaloza, eds., Proceedings of the 29th International Workshop on Description Logics (DL'16), volume 1577, 2016. CEUR Workshop Proceedings

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{MPR2016,
  author    = {Norbert Manthey and Rafael Pe{\~{n}}aloza and Sebastian Rudolph},
  title     = {Efficient Axiom Pinpointing in {EL} using {SAT} Technology},
  editor    = {Maurizio Lenzerini and Rafael Pe{\~{n}}aloza},
  booktitle = {Proceedings of the 29th International Workshop on Description
               Logics (DL'16)},
  volume    = {1577},
  publisher = {CEUR Workshop Proceedings},
  year      = {2016}
}