Oliver Fernandez Gil (TU Dresden, Germany)
Unification in Description Logics has been proposed as a novel inference service that can be used to detect redundancies in ontologies. In this course, we will give a survey of the results on unification in description logics and present the relevant open problems in the field. We will study the computational complexity of the corresponding decision problem in different description logics and conduct a thorough presentation of the techniques that have been develop to solve them.
In addition, we will discuss the connection to the closely related area of modal logics, where unification has been investigated as a special case of recognizability of admissible inference rules. The relevance of the problem in this area will be highlighted, and the most important results and open problems will be presented.