Resolution-based calculi for modal and temporal logics

Abstract

In this paper a technique is presented which provides us with a means to develop resolution-based calculi for (first-order) modal and temporal logics. The approach is based on three parts: A special translation technique from modal and temporal logic formulae into classical predicate logic, a certain kind of saturation technique which is to be applied to given background theories, and an extraction of either suitable “simpler” background theories or logic-specific inference rules. The former is interesting in case existing classical logic theorem provers are to be utilized; the latter gains importance if one is prepared to extend theorem provers that are already at hand.