SAT-Encoding of Unification in ELH_R^+ w.r.t. Cycle-Restricted Ontologies

Franz BaaderFranz Baader, Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska

Download

Franz Baader, Stefan Borgwardt, Barbara Morawska
SAT-Encoding of Unification in ELH_R^+ w.r.t. Cycle-Restricted Ontologies
Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), volume 7364 of Lecture Notes in Artificial Intelligence, 30-44, 2012. Springer

Details
Bibtex

KurzfassungAbstract
Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic EL, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for EL based on a translation into propositional satisfiability (SAT) has recently been presented. In this paper, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t. ELHR+-ontologies.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaBM-IJCAR-12,
  address = {Manchester, UK},
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  booktitle = {Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12)},
  pages = {30--44},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {{SAT}-Encoding of Unification in {$\mathcal{ELH}_{R^+}$} w.r.t. Cycle-Restricted Ontologies},
  volume = {7364},
  year = {2012},
}