Unification in the Description Logic EL

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

Unification in the Description Logic EL

Franz BaaderFranz Baader,  Barbara MorawskaBarbara Morawska
Franz Baader, Barbara Morawska
Unification in the Description Logic EL
Logical Methods in Computer Science, 6(3), 2010
  • KurzfassungAbstract
    Abstract:

    The Description Logic 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, 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 EL is decidable. More precisely, EL-unification is NP-complete, and thus has the same complexity as EL-matching.

    We also show that, w.r.t. the unification type, 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.
  • Bemerkung: Note: Special Issue of the 20th International Conference on Rewriting Techniques and Applications; also available at http://arxiv.org/abs/1006.2289
  • Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@article{ Ba-Mo-LMCS-10,
  author = {Franz {Baader} and Barbara {Morawska}},
  journal = {Logical Methods in Computer Science},
  note = {Special Issue of the 20th International Conference on Rewriting Techniques and Applications; also available at http://arxiv.org/abs/1006.2289},
  number = {3},
  title = {Unification in the Description Logic {$\mathcal{EL}$}},
  volume = {6},
  year = {2010},
}