In this paper we present a framework for the combination of modal and
temporal logic. This framework allows us to combine different normal
forms, in particular, a separated normal form for temporal logic and
a first-order clausal form for modal logics. The calculus of the
framework consists of temporal resolution rules and standard
first-order resolution rules.
We show that the calculus provides a sound,
complete, and terminating inference systems for
arbitrary combinations of subsystems of
multi-modal S5 with linear, temporal logic.