Best unifiers in transitive modal logics (Q647403)

The paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4. There are two views on the origin of the term ``unification'', though both views are very close to each other. Logical unification is the problem to solve whether, for two given formulas, there is a substitution, which makes these formulas equivalent. Unification in computer science is the problem of making two given terms semantically equal. In most cases the problem of term unification directly coincides with its logical unification counterpart. The unification problem is in fact a particular case of a more complicated problem: the substitution problem. That is, the problem whether a formula can be made a theorem after replacing some of the variables by formulas. Ghilardi studied unification in propositional modal logics with the aim of describing all possible unifiers. His approach is very useful in dealing with admissibility. In fact, when a computable finite set of best unifiers is constructed, a solution of the admissibility problem follows immediately. The results of Ghilardi on unification gave a computational ground to construct all unifiers. These techniques turned out to be effective tools to work with various problems. In this paper the author answers positively to the following question: do his previous algorithms for deciding admissibility of inference rules work for the computation of best unifiers in modal transitive logics?