Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25728
Titel: A Resolution-Based Calculus For Temporal Logics
Verfasser: Nonnengart, Andreas
Sprache: Englisch
Erscheinungsjahr: 1995
SWD-Schlagwörter: Temporale Logik ; Prädikatenlogik / Stufe 1
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: The increasing interest in applying temporal logics in various areas of computer science requires the development of efficient means that allow to reason within such logics. Usually this is realized by an implementable calculus and indeed remarkable progress has been made in the last two decades. The approaches developed so far can be roughly divided into two main categories: Either known techniques are extended to cope with the temporal logic syntax, or translation techniques into predicate logic are defined which allow to exploit already existing calculi. The approach proposed in this work is based on a particular translation method into classical first-order predicate logic which utilizes certain interesting translational invariants.
Das ständig wachsende Interesse an Temporallogiken in zahlreichen Gebieten der Informatik verlangt nach Methoden, mit deren Hilfe effizient und schnell Schlussfolgerungen in diesen Logiken gezogen werden können. Üblicherweise geschieht dies durch die Entwicklung eines implementierten Kalküls, und tatsächlich wurden in den vergangenen Jahren bemerkenswerte Fortschritte in diese Richtung erzielt. Die bis heute bekannten Verfahren können grob in zwei Hauptkategorien eingeteilt werden: Entweder werden schon bekannte Techniken für andere Logiken (üblicherweise klassische Prädikatenlogik erster Stufe) erweitert, um mit der neuen Syntax zurechtzukommen, oder Übersetzungstechniken in die Prädikatenlogik werden definiert, welche es erlauben schon bekannte Kalküle wiederzuverwenden. Der Ansatz, der in dieser Arbeit vorgestellt wird, basiert auf einer bestimmten Übersetzungsmethode in die klassische Prädikatenlogik erster Stufe und einem darauf aufbauenden Kalkül, der gewisse interessante Übersetzungsvarianten ausnützt.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-2162
hdl:20.500.11880/25784
http://dx.doi.org/10.22028/D291-25728
Erstgutachter: Priv. Doz. Hans Jürgen Ohlbach
Tag der mündlichen Prüfung: 21-Dez-1995
SciDok-Publikation: 6-Mai-2004
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
AndreasNonnengart_PrivDozDrHansJuergenOhlbach.pdf2,17 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.