zbMATH — the first resource for mathematics

Unification in modal and description logics. (English) Zbl 1258.03018
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.
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.
Reviewer: Nail Zamov (Kazan)

03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)
68Q42 Grammars and rewriting systems
68T27 Logic in artificial intelligence
PDF BibTeX Cite
Full Text: DOI