@INCOLLECTION{Ganzinger-et-al-01-AIML,
 AUTHOR    = {Ganzinger, Harald and Hustadt, Ullrich and Meyer, Christoph
 and Schmidt, Renate A.},
 EDITOR    = {Zakharyaschev, Michael and Segerberg, Krister and 
 de Rijke, Maarten and Wansing, Heinrich},
 TITLE     = {A Resolution-Based Decision Procedure for Extensions of K4},
 BOOKTITLE = {Advances in Modal Logic, Volume 2},
 PUBLISHER = {CSLI},
 YEAR      = {2001},
 VOLUME    = {119},
 CHAPTER   = {9},
 PAGES     = {225--246},
 SERIES    = {CSLI Lecture Notes},
 ADDRESS   = {Stanford, USA},
 ISBN      = {1-57586-272-7},
 URL	   = {\hgURL{~hg/pca.html#Ganzinger-et-al-00-AIML}},
 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 K4, KD4 and S4
can be transformed into a bounded class of well-structured clauses
closed under ordered resolution and negative chaining.},
}