Normal Forms and Proofs in Combined Modal and Temporal Logics

Hustadt, U., Dixon, C., Schmidt, R. A. and Fisher, M. (2000)

In H. Kirchner and C. Ringeissen (eds), Proceedings of the International Workshop on Frontiers of Combining Systems (FroCoS'2000). Lecture Notes in Artificial Intelligence 1794, Springer, 73-87. BiBTeX, PostScript (Copyright © Springer).

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.

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 30 Apr 2001
Copyright © 2000 Renate A. Schmidt, School of Computer Science, Man Univ,