de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Book Chapter

Resolution is a Decision Procedure for Many Propositional Modal Logics

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45401

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

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

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: http://hdl.handle.net/11858/00-001M-0000-000F-3878-C
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.