Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies
Franz Baader, Oliver Fernández Gil · 2024
Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies.In particular, it was shown that testing unifiability in the DL EL is an NP-complete problem, and this result has been extended in several directions.Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions.Motivated by features of the medical ontology SNOMED CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms.We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.Description Logics (DLs) [11] are a prominent family of logic-based knowledge representation languages, which offer their users a good compromise between expressiveness and complexity of reasoning, and constitute the formal and algorithmic foundation of the standard Web Ontology Language OWL 2. 1 The DL EL, which provides the concept constructors conjunction (u), existential restriction (9r.C), and top concept (>), is a rather inexpressive, but nevertheless very useful member of this family.On the one hand, the important reasoning problems, such as the subsumption and the equivalence problem, in EL and some of its extensions are decidable in polynomial time [23,8].On the other hand, EL and its tractable extensions are frequently used to define biomedical ontologies, such as the large medical ontology SNOMED CT. 2 To illustrate the use of the top concept, whose absence plays an important rôle in this paper, consider the EL concept descriptions Man u 9child .>and Man u 9child .Female of the concepts Father and Father of a daughter, respectively.In the former description, the top concept is used since no further properties of the child are to be required.Unification in DLs has been introduced in [18] as a new inference service, motivated by the need for detecting redundancies in ontologies, in a setting where different ontology engineers (OEs) constructing the ontology may model the same concepts on different levels of granularity.For example, assume that (using the style of SNOMED CT definitions) one OE models the concept of a viral infection of the lung as ViralInfection u 9findingSite.LungStructure,