A syntax transformation is presented that eliminates the modal logic operators from modal logic formulae by shifting the modal context information to the term level. The formulae in the transformed syntax can be brought into conjunctive normal form such that a clause based resolution calculus without any additional inference rule, but with special modal unification algorithms, can be defined. The method works for first-order modal logics with the two operators □ and ♦ and with constant-domain Kripke semantics where the accessibility relation is serial and may have any combination of the following properties: reflexivity, symmetry, transitivity. In particular the quantified versions of the modal systems T, S4, S5, B, D, D4 and DB can be treated. Extensions to non-serial and varying-domain systems are possible, but not presented here.