Unification in modal and description logics (Q2889571)

Unification, i.e. the problem of making given terms syntactically equal by replacing their variables by terms, was originally introduced in automated deduction and term rewriting. In addition to the ``classical'' applications of unification, unification has also turned out to be of interest in other areas.NEWLINENEWLINE In this article the authors consider two closely related, yet different application areas for unification: modal logics and description logics. These areas are closely related since many description logics are just syntactic variants of certain modal logics. Consequently, technical results obtained in one area can be translated to the other. In most cases unification problems in modal logics and in description logics can actually be viewed as unification problems modulo the equational theory that axiomatizes equivalence in the respective logic. The authors explain the connection between description and modal logics. Then they show how unification problems can be viewed as equational unification problems. Some open problem for unification in modal logic is discussed.