Hybrid Unification in the Description Logic EL

Unification in Description Logics (DLs) has been proposed as an in-ference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. However, the unification algorithms for EL developed until recently could not deal with ontologies containing general concept inclusions (GCIs). In a series of recent papers we have made some progress towards addressing this problem, but the ontologies the de-veloped unification algorithms can deal with need to satisfy a certain cycle restriction. In the present paper, we follow a different approach. Instead of restricting the input ontologies, we generalize the notion of unifiers to so-called hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics that combines fix-point and descriptive semantics. We show that hybrid unification in EL is NP-complete and introduce a goal-oriented algorithm for computing hybrid unifiers