@INCOLLECTION{GanzingerHustadtMeyerSchmidt01,
AUTHOR = {Ganzinger, H. and Hustadt, U. and Meyer, C. and Schmidt, R. A.},
YEAR = {2001},
TITLE = {A Resolution-Based Decision Procedure for Extensions of {K4}},
EDITOR = {Zakharyaschev, M. and Segerberg, K. and de Rijke, M. and Wansing, H.},
BOOKTITLE = {Advances in Modal Logic, Volume 2},
SERIES = {Lecture Notes},
VOLUME = {119},
PUBLISHER = {CSLI Publications},
ADDRESS = {Stanford},
PAGES = {225--246},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/GanzingerHustadtMeyerSchmidt01.html},
ABSTRACT = {
This paper presents a resolution decision procedure for transitive
propositional modal logics.
The procedure combines the relational translation method with an
ordered chaining calculus designed to avoid unnecessary
inferences with transitive relations.
We show the logics $\mathsf{K4}$, $\mathsf{KD4}$ and $\mathsf{S4}$
can be transformed into a bounded class of well-structured clauses
closed under ordered resolution and negative chaining.  
}}