Unification in first-order transitive modal logic

We introduce unification in first-order transitive modal logics, i.e. logics extending Q-K4, and apply it to solve some problems such as admissibility of rules. Unifiable formulas in some extensions of Q-K4 are characterized and an explicit basis for the passive rules (those with non-unifiable premises) is provided. Both unifiability and passive rules depend on the number of logical constants in the logic; we focus on extensions of Q-K4 with at most four constants inverted perpendicular, perpendicular to, square perpendicular to, lozenge inverted perpendicular. Projective formulas, defined in a way similar to propositional logic, are used to solve some questions concerning the disjunction and existence properties. A partial characterization of first-order modal logics with projective unification is given. Then logics with filtering unification are characterized and the unification type of certain logics extending Q-K4.2 and Q-K4.3 is settled. To this aim the weak existence property is adapted for first-order modal logics.