Unification in transitive reflexive modal logics

Abstract

This paper contains a proof-theoretic account of unification in (fragments of) transitive reflexive modal logics, which means that the reasoning is syntactic and uses as little semantics as possible. New proofs of theorems on unification types are given and these results are extended to fragments. It is shown that transitive reflexive fragments that contain at least implication and conjunction have finitary unification, and that in the absence of disjunction they have unitary unification. The relation between classical valuations and projective unifiers is clarified, and it is shown that also in fragments the Visser rules form a basis for the admissible rules once they are admissible.