Unification in Modal and Description Logics

Unification is the problem of making two given terms syntactically equal by replacing their variables by terms. It was formally (and independently) introduced in automated deduction by J. A. Robinson and in term rewriting by Knuth and Bendix, as a key component of the resolution inference principle and the Knuth-Bendix completion procedure. Early research on (syntactic) unification and its generalizations set the basis for the development to what is nowadays known as unification theory, a research area that has found many applications in other areas, including Description Logic and Modal Logics.

The aim of this course is to review the most important results on unification in description and modal logics. We will study the computational complexity of the corresponding decision problem in different description logics, analyze the techniques that have been devised to solve them and present the relevant open problems in the area. On the modal logic side, the relevance of unification in this area will be highlighted, and the most important results and open problems will be presented. In addition, we will briefly discuss the correspondence between description and modal logics, and how this correspondence relates the respective notions of unification.

Pre-existing knowledge about unification theory, description logics and modal logics is not required for attending this course. All the relevant notions will be introduced during the lecture.