Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

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

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Schmidt, Renate A.dblp

BibTeX cite key*:

Schmidt99a

Title

Title*:

Decidability by Resolution for Propositional Modal Logics

Journal

Journal Title*:

Journal of Automated Reasoning
Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Kluwer
Publisher's URL:


Publisher's
Address:


ISSN:


Vol, No, pp, Date

Volume*:

22
Number:

4

Publishing Date:

May 1999

Pages*:

379-396
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

The paper shows that satisfiability in a range of popular propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution combined with condensing, and possibly some additional form of normalisation, is a decision procedure for the satisfiability problem in certain so-called path logics. Path logics arise from normal propositional modal logics by the optimised functional translation method. The decision result provides an alternative method of proving decidability for modal logics, as well as closely related systems of artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, any fair implementation of a first-order theorem prover which is based on resolution is suitable for facilitating modal reasoning.

URL for the Abstract:


Categories,
Keywords:

Theorem Proving, Modal Logic

HyperLinks / References / URLs:

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

Copyright Message:


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:
@ARTICLE{Schmidt99a,
AUTHOR = {Schmidt, Renate A.},
 TITLE = {Decidability by Resolution for Propositional Modal Logics},
 JOURNAL = {Journal of Automated Reasoning},
 PUBLISHER = {Kluwer},
 YEAR = {1999},
 NUMBER = {4},
 VOLUME = {22},
 PAGES = {379--396},
 MONTH = {May},
}

Entry last modified by Renate A. Schmidt, 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/21/1999 07:16:16 PM
Revision
0.



Editor
Renate A. Schmidt



Edit Date
21/04/99 19:16:16