guest ::
Guarded logics : algorithms and bisimulation
2002
Aachen, Techn. Hochsch., Diss., 2002
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
Tag der mündlichen Prüfung/Habilitation
2002-07-17
Online
URN: urn:nbn:de:hbz:82-opus-4550
URL: https://publications.rwth-aachen.de/record/57153/files/Hirsch_Colin.pdf
Einrichtungen
Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; mathematische Logik (frei) ; Modelltheorie (frei) ; Bisimulation (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
In vielen praktischen Anwendungen logik-basierter Methoden besteht die Notwendigkeit Ausdrucksstaerke und Berechenbarkeitskomplexitaet gegeneinander abzuwaegen. Sowohl das auffinden entscheidbarer Teilklassen der Praedikatenlogik erster Stufe, als auch Erweiterungen der Modallogik zu maechtigeren, aber nach wie vor effizient handhabbaren logischen Sprachen, sind ein wesentliches Forschungsziel. Das bewachte Fragment der Praedikatenlogik erster Stufe stellt einen erfolgreichen Versuch dar, die entscheidenden Eigenschaften von Modal-, Temporal- und Entscheidungslogiken auf ein groesseres Fragment der Praedikatenlogik zu verallgemeinern. Neben der Entscheidbarkeit gehoeren dazu die Endliche-Modell-Eigenschaft, die Invarianz unter einem geeigneten Bisimulationsbegriff und andere modelltheoretische Eigenschaften wie eine entscheidbare Erweiterung um Fixpunkte. Das Ziel dieser Arbeit besteht darin ein groesseres Verstaendnis in die Uebereinstimmung zwischen dem modalen und dem bewachten Ansatz zu finden. Dabei wurden einige elementare, und typischerweise sehr modale Eigenschaften betreffende, Luecken in den Ergebnissen ueber bewachte Logiken geschlossen. Eine bewachte Logik zweiter Stufe sowie eine bewachte relationale Algebra werden eingefuehrt. Eine dabei in verschiedenen Zusammenhaengen benutzte Technik besteht darin Strukturen und Formeln der bewachten Welt in ihre modalen Entsprechungen zu ueberfuehren. Dies ermoeglicht den Transfer einiger Resultate unter gleichzeitiger Ermoeglichung tieferer Einblicke in die Natur bewachter Logiken. Betrachtete Themengebiete umfassen Tableau basierte Entscheidungsverfahren, eine Landkarte aktions-bewachter Logiken, Kanonisierung von Strukturen und modelltheoretische Charakterisierungen.For many practical applications of logic-based methods there is a requirement to balance expressive power against computational tractability. Both identifying decidable sub-classes of first-order logic, and extending modal logic to larger, but nevertheless efficiently solvable languages has been a preeminent goal of research. The guarded fragment of first-order logic was a successful attempt to transfer key tractability properties of modal, temporal, and description logics to a larger fragment of predicate logic. Besides decidability, guarded logics inherit the finite model property, invariance under an appropriate variant of bisimulation, and other nice model theoretic properties including a decidable fixed-point extension. The goal of this this work is to gain greater insight into the correspondence between the modal world and the guarded world. In this process, several gaps concerning basic, typically modal, features of guarded logics are closed. Guarded second order logic and guarded relational algebra are developed. A recurring key technique consists of encoding structures and formulae used in the guarded world as their modal counterparts. This enables the transfer of various results, as well as giving greater insight into the nature of guarded logics. Touched subjects include tableau-based decision procedures, mapping action guarded logics, canonisation of structures and model-theoretic characterisation theorems.
Fulltext: 
PDF
(additional files)
Dokumenttyp
Dissertation / PhD Thesis
Format
online, print
Sprache
English
Externe Identnummern
HBZ: HT013539134
Interne Identnummern
RWTH-CONV-119220
Datensatz-ID: 57153
Beteiligte Länder
Germany
|
The record appears in these collections: |