@INCOLLECTION{Schmidt98f,
AUTHOR = {Schmidt, R. A.},
YEAR = {1998},
TITLE = {Resolution is a Decision Procedure for Many Propositional Modal Logics},
EDITOR = {Kracht, M. and de Rijke, M. and Wansing, H. and Zakharyaschev, M.},
BOOKTITLE = {Advances in Modal Logic, Volume 1},
SERIES = {Lecture Notes},
VOLUME = {87},
PUBLISHER = {CSLI Publications},
ADDRESS = {Stanford},
PAGES = {189--208},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/Schmidt98f.html},
ISBN = {1-57586-103-8 (hardback), 1-57586-102-X (paper)},
ABSTRACT = {The paper shows satisfiability in many propositional modal systems,
including \textit{K}, \textit{KD}, \textit{KT} and \textit{KB}, their
combinations as well as their multi-modal versions, 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 \emph{path logics}.
Path logics arise from propositional and normal
uni- and multi-modal logics by the \emph{optimised functional
translation} method.
The decision result provides an alternative decision proof for the
relevant modal systems, and related systems in artificial intelligence.
However, this alone is not very 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.
}}