The paper shows satisfiability in many propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution and condensing is a decision procedure for the satisfiability problem of formulae in so-called path logics. Path logics arise from propositional and normal uni- and multi-modal logics by the optimised functional translation method. The decision result provides an alternative decision proof for the relevant modal logics (including K, KD, KT and KB, their combinations as well as their multi-modal versions), and related systems in artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, any standard first-order theorem prover that is based on resolution can serve as a reasonable and efficient inference tool for modal reasoning.
The short version is published in Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds) (1998), Advances in Modal Logic, Volume 1, Lecture Notes 87, CSLI Publications, Stanford, 189-208. Abstract, BiBTeX.