The Description Logic EL has recently drawn considerable attention since, onthe one hand, important inference problems such as the subsumption problem arepolynomial. On the other hand, EL is used to define large biomedicalontologies. Unification in Description Logics has been proposed as a novelinference service that can, for example, be used to detect redundancies inontologies. The main result of this paper is that unification in EL isdecidable. More precisely, EL-unification is NP-complete, and thus has the samecomplexity as EL-matching. We also show that, w.r.t. the unification type, ELis less well-behaved: it is of type zero, which in particular implies thatthere are unification problems that have no finite complete set of unifiers.
展开▼
