06076896

a

06076896 Baader, Franz Borgwardt, Stefan Morawska, Barbara SAT encoding of unification in $\mathcal{ELH}_{{R}^+}$ w.r.t. Cycle-restricted ontologies. Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 30-44 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-31365-3_5

Summary: 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 $\mathcal{EL}$, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for $\mathcal{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 ($\mathcal{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. $\mathcal{ELH}_{{R}^+}$-ontologies.