Normal forms and proofs in combined modal and temporal logics

Abstract

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 termina-ting inference systems for arbitrary combinations of subsystems of multi- modal S5 with linear, temporal logic.