Unifiers in transitive modal logics for formulas with coefficients (meta-variables)
Vladimir Vladimirovich Rybakov · Logic Journal of IGPL · 2012
In this article we study and solve some open problem of unification for formulas with coefficients (meta-variables) in transitive modal logics. The role of coefficients is played by propositional letters which are constants (which any unifier lets intact). We solve this problem affirmatively: we find an algorithm which constructs a finite set of the best unifiers for any unifiable formula with coefficients. This algorithm works for all transitive modal logics satisfying special general conditions. These conditions hold, in particular, for modal logics K4, S4, Grz and GL, so our results are true for these important logics. In terms of algebraic logic (or universal algebra), we solve the problem of finding solutions for equations in the free modal algebras in the signature extended by constants for free variables.