Your search returned the following document:

1. A Resolution-Based Decision Procedure for Extensions of K4
   Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, and Renate A. Schmidt
   In: Advances in Modal Logic, Volume 2, 2001, 225-246
   [PS: Download: _01AIML.ps.gz]