Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26295
Titel: Incremental decision procedures for modal logics with nominals and eventualities
Alternativtitel: Inkrementelle Entscheidungsverfahren für Modallogiken mit Nominalen und Eventualities
VerfasserIn: Kaminski, Mark
Sprache: Englisch
Erscheinungsjahr: 2012
Kontrollierte Schlagwörter: Entscheidungsverfahren
Tableau <Logik>
Dynamische Aussagenlogik
Computational logic
Modallogik
Automatisches Beweisverfahren
Freie Schlagwörter: Hybridlogik
Nominale
Temporallogik
decision procedures
automated reasoning
tableau systems
propositional dynamic logic
modal logic
hybrid logic
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Dissertation
Abstract: This thesis contributes to the study of incremental decision procedures for modal logics with nominals and eventualities. Eventualities are constructs that allow to reason about the reflexive-transitive closure of relations. Eventualities are an essential feature of temporal logics and propositional dynamic logic (PDL). Nominals extend modal logics with the possibility to reason about state equality. Modal logics with nominals are often called hybrid logics. Incremental procedures are procedures that can potentially solve a problem by performing only the reasoning steps needed for the problem in the underlying calculus. We begin by introducing a class of syntactic models called demos and showing how demos can be used for obtaining nonincremental but worst-case optimal decision procedures for extensions of PDL with nominals, converse and difference modalities. We show that in the absence of nominals, such nonincremental procedures can be refined into incremental demo search procedures, obtaining a worst-case optimal decision procedure for modal logic with eventualities. We then develop the first incremental decision procedure for basic hybrid logic with eventualities, which we eventually extend to deal with hybrid PDL. The approach in the thesis suggests a new principled design of modular, incremental decision procedures for expressive modal logics. In particular, it yields the first incremental procedures for modal logics containing both nominals and eventualities.
Diese Dissertation untersucht inkrementelle Entscheidungsverfahren für Modallogiken mit Nominalen und Eventualities. Eventualities sind Konstrukte, die erlauben, über den reflexiv-transitiven Abschluss von Relationen zu sprechen. Sie sind ein Schlüsselmerkmal von Temporallogiken und dynamischer Aussagenlogik (PDL). Nominale erweitern Modallogik um die Möglichkeit, über Gleichheit von Zuständen zu sprechen. Modallogik mit Nominalen nennt man Hybridlogik. Inkrementell ist ein Verfahren dann, wenn es ein Problem so lösen kann, dass für die Lösung nur solche Schritte in dem zugrundeliegenden Kalkül gemacht werden, die für das Problem relevant sind. Wir führen zunächst eine Klasse syntaktischer Modelle ein, die wir Demos nennen. Wir nutzen Demos um nichtinkrementelle aber laufzeitoptimale Entscheidungsverfahren für Erweiterungen von PDL zu konstruieren. Wir zeigen, dass im Fall ohne Nominale solche Verfahren durch algorithmische Verfeinerung zu inkrementellen Verfahren ausgebaut werden können. Insbesondere erhalten wir so ein optimales Verfahren für Modallogik mit Eventualities. Anschließend entwickeln wir das erste inkrementelle Verfahren für Hybridlogik mit Eventualities, welches wir schließlich auf hybrides PDL erweitern. Die Dissertation vermittelt einen neuen Ansatz zur Konstruktion modularer, inkrementeller Entscheidungsverfahren für expressive Modallogiken. Insbesondere liefert der Ansatz die ersten inkrementellen Verfahren für Modallogiken mit Nominalen und Eventualities.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-46765
hdl:20.500.11880/26351
http://dx.doi.org/10.22028/D291-26295
Erstgutachter: Smolka, Gert
Tag der mündlichen Prüfung: 24-Jan-2012
Datum des Eintrags: 8-Feb-2012
Fakultät: MI - Fakultät für Mathematik und Informatik
Fachrichtung: MI - Informatik
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
thesis_print.pdf1,32 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.