Rijke. Resolution in modal, description and hybrid logic

We provide a resolution-based proof procedure for modal, description and hybrid logic that improves on previous proposals in important ways. It avoids translations into large unde-cidable logics, and works directly on modal, description or hybrid 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