Unification in Description Logics for Avoiding Redundancies in Medical Ontologies

描述逻辑中的统一原则上可以用来检测并避免本体中的冗余。然而，用于此目的的统一过程的使用受到这样一个事实的阻碍，即只有对于非表达性描述逻辑FL0才知道肯定的结果，其中没有制定实际的本体，并且统一问题的复杂性相当高。在提交原始提案之前，我们能够为DescriptionLogic EL开发一个统一过程，并且可以证明EL中统一的复杂性低于FL0 （NP-complete与ExpTime-complete）。尽管EL也是一种缺乏表达的描述逻辑，但它比FL0更适合应用程序。特别是，一些完善的医学本体（如SNOMED CT）是用EL编写的。前一个项目的目标一方面是开发和实现一个实用的EL统一程序，并评估其在SNOMED CT扩展中寻找冗余的应用。另一方面，我们希望为EL的应用程序相关扩展开发统一过程。特别是，我们打算研究统一模一般概念包含（gci）。虽然我们在之前的项目中获得了各种有趣的结果，但提案中提到的一些问题比预期的要困难（但也更有趣）。特别地，我们只得到了一般概念包含的统一模的部分结果。从应用程序的角度来看，我们遇到的问题是，给定的统一问题可能有大量的统一器，其中许多可能与寻找冗余无关。因此，我们必须开发计算更少且相关的统一器的方法。在项目的第二阶段，我们希望解决这些遗留问题。此外，我们想研究最近认识到的与统一理论（刚性e统一，不统一）和模态逻辑（可接受推理规则）问题的联系。我们还将继续研究统一在本体中寻找冗余的应用，基于改进的计算统一器的过程。此外，我们现在还将考虑FL0扩展中的统一。事实上，由于最近的两个结果，这样做的先决条件已经大大改善。

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.