Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse




Book Chapter

Resolution is a Decision Procedure for Many Propositional Modal Logics


Schmidt,  Renate A.
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Schmidt, R. A. (1998). Resolution is a Decision Procedure for Many Propositional Modal Logics. In M. Kracht, M. de Rijke, H. Wansing, & M. Zakharyaschev (Eds.), Advances in Modal Logic, Volume 1 (pp. 189-208). Stanford, USA: CSLI.

Cite as:
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.