Resolution in Modal, Description and Hybrid Logic
Carlos Areces, Hans de Nivelle, Maarten de Rijke

Abstract:
We provide a resolution-based proof procedure for modal, description
and hybrid logic that improves on previous proposals in important
ways.  It avoids translation into large undecidable logics, and works
directly on modal, description or hybird logic formulas instead.  In
addition, by using the hybrid machinery it avoids the complexities of
earlier propositional resolution-based methods for modal logic.  It
combines ideas from the method of prefixes used in tableaux, and
resolution ideas in such a way that some of the heuristics and
optimizations devised in either field are applicable.