A Goal-Oriented Algorithm for Unification in EL w.r.t. Cycle-Restricted TBoxes.
Franz Baader, Stefan Borgwardt, Barbara Morawska · 2012
Unification in DLs has been proposed in [7] (for the DL FL0, which offers the constructors conjunction (⊓), value restriction (∀r.C), and the top concept (⊤)) as a novel inference service that can, for instance, be used to detect redundancies in ontologies. For example, assume that one developer of a medical ontology