Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse
  1. Datensatz ansehen / 
  2. Datensatz Übersicht

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Buchkapitel

A Resolution-Based Decision Procedure for Extensions of K4

MPG-Autoren
/persons/resource/persons44474

Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44660

Hustadt,  Ullrich
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44784

Meyer,  Christoph
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45401

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

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Ganzinger, H., Hustadt, U., Meyer, C., & Schmidt, R. A. (2001). A Resolution-Based Decision Procedure for Extensions of K4. In M. Zakharyaschev, K. Segerberg, M. de Rijke, & H. Wansing (Eds.), Advances in Modal Logic, Volume 2 (pp. 225-246). Stanford, USA: CSLI.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-31DD-B
Zusammenfassung
This paper presents a resolution decision procedure for transitive propositional modal logics. The procedure combines the relational translation method with an ordered chaining calculus designed to avoid unnecessary inferences with transitive relations. We show the logics K4, KD4 and S4 can be transformed into a bounded class of well-structured clauses closed under ordered resolution and negative chaining.