Unification in Description Logics for Avoiding Redundancies in Medical Ontologies

点击翻译按钮获取中文摘要

Unification in Description Logics can in principle be used to detect and thus avoid redundancies in ontologies. The use of unification procedures for this purpose was, however, hindered by the fact that positive results were only known for the inexpressive Description Logic FL0, in which no practical ontologies are formulated and for which the complexity of the unification problem is quite high. Beforesubmission of the original proposal we were able to develop a unification procedure for the DescriptionLogic EL and could show that the complexity of unification in EL is lower than in FL0 (NP-complete versus ExpTime-complete). Although EL is also an inexpressive Description Logic, it is more relevant for applications than FL0. In particular, several well-established medical ontologies (such as SNOMED CT) are written in EL. The goal of the predecessor project was on the one hand to develop and implement a practical unification procedure for EL and to evaluate it on the application of finding redundancies in extensions of SNOMED CT. On the other hand, we wanted to develop unification procedures for application-relevant extensions of EL. In particular, we intended to investigate unification modulo general concept inclusions (GCIs).Although we have obtained a variety of interesting results in the predecessor project, an number of problems mentioned in the proposal turned out to be harder (but also more interesting) than expected. In particular, we have only obtained partial results for unification modulo general concept inclusions. From the application point of view, we encountered the problem that a given unification problem may have a high number of unifiers, of which many may be irrelevant for finding redundancies. Thus, we have to develop methods that compute fewer and relevant unifiers. In the second phase of the project we want to solve these remaining problems. In addition we want to investigate only recently recognized connections to problems from unification theory (rigid E-unification, disunification) and modal logics (admissible inference rules). We will also continue to investigate the application of unification for finding redundancies in ontologies, based on improved procedures for computing unifiers. In addition, we will now also consider unification in extensions of FL0. In fact, the preconditions for this have considerably improved due to two recent results.