About the unification type of modal logics between KB and KTB

International audienceThe unification problem in a normal modal logic is to determine, given a formula φ, whether there exists a substitution σ such that σ(φ) is in that logic. In that case, σ is a unifier of φ. We shall say that a set of unifiers of a unifiable formula φ is minimal complete if for all unifiers σ of φ, there exists a unifier τ of φ in that set such that τ is more general than σ and for all σ,τ in that set, σ≠τ, neither σ is more general than τ, nor τ is more general than σ. When a unifiable formula has no minimal complete set of unifiers, the formula is nullary. We usually distinguish between elementary unification and unification with parameters. In elementary unification, all variables are likely to be replaced by formulas when one applies a substitution. In unification with parameters, some variables—called parameters—remain unchanged. In this paper, we prove that normal modal logics KB, KDB and KTB as well as infinitely many normal modal logics between KDB and KTB possess nullary formulas for unification with parameters