Part, Chapter of a Book
@InBook, Buchkapitel
Beitrag im Sammelband


Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor
Author(s):
Schmidt, Renate A.dblp
Editor(s):
Kracht, M.
de Rijke, M.
Wansing, H.
Zakharyaschev, M.		dblp
dblp
dblp
dblp

BibTeX cite key*:

Schmidt98f

Title, Booktitle

Title*:

Resolution is a Decision Procedure for Many Propositional Modal Logics

Booktitle*:

Advances in Modal Logic, Volume 1

Chapter:

13

Series:

CSLI Lecture Notes

Language:

English

Publisher

Name*:

CSLI
URL:


Address*:

Stanford, USA
Publication Type:


Vol, No, pp., Year

Volume:

87
Number:


Edition:


Pages*:

189-208

Month:

April
VG Wort Pages:


ISBN:

1-57586-103-8 (hardback); 1-57586-102-X (paper)
Year*:

1998

Abstract, Links, ©

Note:


LaTeX 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.

URL Abstract:


Tags, Keywords:

modal logic, translation methods, optimised functional translation, resolution decision procedures

Copyright Message:


HyperLinks / References / URLs:

http://www.doc.mmu.ac.uk/STAFF/R.Schmidt/publications/Schmidt98f.html

Personal Comments:


Download
Access Level:


Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat
BibTeX Entry:
@INBOOK{Schmidt98f,
AUTHOR = {Schmidt, Renate A.},
 EDITOR = {Kracht, M. and de Rijke, M. and Wansing, H. and Zakharyaschev, M.},
 TITLE = {Resolution is a Decision Procedure for Many Propositional Modal Logics},
 BOOKTITLE = {Advances in Modal Logic, Volume 1},
 PUBLISHER = {CSLI},
 YEAR = {1998},
 VOLUME = {87},
 CHAPTER = {13},
 PAGES = {189--208},
 SERIES = {CSLI Lecture Notes},
 ADDRESS = {Stanford, USA},
 MONTH = {April},
 ISBN = {1-57586-103-8 (hardback)},
; ISBN = {1-57586-102-X (paper)},
}

Entry last modified by Uwe Brahm, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Renate A. Schmidt		Created
04/14/1998 09:27:35 PM
Revisions
4.
3.
2.
1.
0.		Editor(s)
Uwe Brahm
Uwe Brahm
Renate A. Schmidt
Renate A. Schmidt
Renate A. Schmidt		Edit Dates
01.04.99 17:34:54
01.04.99 09:45:18
14/04/98 21:31:39
14/04/98 21:29:58
14/04/98 21:27:36