 |
    |
A Goal-Oriented Algorithm for Unification in 
w.r.t. Cycle-Restricted Ontologies*
Franz Baader, Stefan Borgwardt, and Barbara Morawska
Theoretical Computer Science, TU Dresden, Germanybaader@tcs.inf.tu-dresden.de
stefborg@tcs.inf.tu-dresden.de
morawska@tcs.inf.tu-dresden.de
Abstract. Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL 
, which is used to define several large biomedical ontologies, unification is NP-complete. A goal-oriented NP unification algorithm for 
that uses nondeterministic rules to transform a given unification problem into solved form has recently been presented. In this paper, we extend this goal-oriented algorithm in two directions: on the one hand, we add general concept inclusion axioms (GCIs), and on the other hand, we add role hierarchies (
) and transitive roles (R + ). For the algorithm to be complete, however, the ontology consisting of the GCIs and role axioms needs to satisfy a certain cycle restriction.
*Supported by DFG under grant BA 1122/14-1.
LNAI 7691, p. 493 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2012