@INPROCEEDINGS{Nonnengart-CADE96,
AUTHOR = {Andreas Nonnengart},
TITLE = {Resolution-Based Calculi for Modal and Temporal Logics},
BOOKTITLE = {Proceedings of the 13th International Conference on Automated Deduction, CADE 13},
YEAR = {1996},
EDITOR = {M.A.~McRobbie and J.K.~Slaney},
PAGES = {598-612},
PUBLISHER = {Springer, LNAI 1104},
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.},
}