Extending unification in EL towards general TBoxes
Franz Baader, Stefan Borgwardt, Barbara Morawska · 2012
Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to de-tect redundancies in ontologies. The inexpressive Descrip-tion Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are de-fined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of signifi-cantly lower complexity than unification in other DLs of sim-ilarly restricted expressive power. However, the unification algorithms for EL developed so far cannot deal with general concept inclusion axioms (GCIs). This paper makes a consid-erable step towards addressing this problem, but the GCIs our new unification algorithm can deal with still need to satisfy a certain cycle restriction. 1