2009 | OriginalPaper | Buchkapitel
Unification in the Description Logic
verfasst von : Franz Baader, Barbara Morawska
Erschienen in: Rewriting Techniques and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The Description Logic
$\mathcal{EL}$
has recently drawn considerable attention since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand,
$\mathcal{EL}$
is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The main result of this paper is that unification in
$\mathcal{EL}$
is decidable. More precisely,
$\mathcal{EL}$
-unification is NP-complete, and thus has the same complexity as
$\mathcal{EL}$
-matching. We also show that, w.r.t. the unification type,
$\mathcal{EL}$
is less well-behaved: it is of type zero, which in particular implies that there are unification problems that have no finite complete set of unifiers.