English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Resolution is a Decision Procedure for Many Propositional Modal Logics

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.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Schmidt, Renate A.1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121998
 Publication Status: Issued
 Pages: -
 Publishing info: Stanford, USA : CSLI
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519652
Other: Local-ID: C1256104005ECAFC-9DD4087B0E8774C4C12565E6006AE588-Schmidt98f
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Advances in Modal Logic, Volume 1
Source Genre: Book
 Creator(s):
Kracht, M., Editor
de Rijke, M., Editor
Wansing, H., Editor
Zakharyaschev, M., Editor
Affiliations:
-
Publ. Info: Stanford, USA : CSLI
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 189 - 208 Identifier: ISBN: 1-57586-103-8 (hardback)

Source 2

show
hide
Title: CSLI Lecture Notes
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 87 Sequence Number: - Start / End Page: - Identifier: -