Unification and passive inference rules for modal logics

Abstract

We 1 study unification of formulas in modal logics and consider logics which are equivolent w.r.t. unification of formulas. A criteria is given for equivalence w.r.t. uniilcation via existence or persistent formulas. A complete syntactic description cf all formulas which are non-unifiable in wide classes of modal logics is given. Passive inference rules are considered, it is shown that in any modal logic over D4 there is a finite basis for passive rules.