Resolution is a decision procedure for many propositional modal logics
Renate A. Schmidt · MPG.PuRe (Max Planck Society) · 1997
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 \\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 logics (including \\textit{K}, \\textit{KD}, \\textit{KT} and \\textit{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.