@ARTICLE{Schmidt99a,
AUTHOR = {Schmidt, R. A.},
YEAR = {1999},
TITLE = {Decidability by Resolution for Propositional Modal Logics},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {22},
NUMBER = {4},
PAGES = {379--396},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/Schmidt99a.html},
ABSTRACT = {The paper shows that satisfiability in a range of popular propositional
modal systems can be decided by ordinary resolution procedures.
This follows from a general result that resolution combined with
condensing, and possibly some additional form of normalisation,
is a decision procedure for the satisfiability problem in certain
so-called path logics.
Path logics arise from normal propositional modal
logics by the optimised functional translation method.
The decision result provides an alternative method of proving
decidability for modal logics,
as well as closely related systems of artificial intelligence.
This alone is not interesting.
A more far-reaching consequence of the result has practical value,
namely, any fair implementation of a first-order theorem prover which
is based on resolution is suitable for facilitating modal reasoning.},
}