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 terminating inference systems for arbitrary combinations of subsystems of multi-modal S5 with linear, temporal logic.
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.
| Original language | Undefined |
|---|---|
| Number of pages | 6 |
| Publication status | Published - 2000 |
Publication series
| Name | Lecture notes in computer science |
|---|---|
| Volume | 1794 |
Keywords
- Modal logic
- Temporal logic
- Inference rule
- linear temporal logic
- Predicate symbol