Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25703
Titel: Resolution-based decision procedures for subclasses of first-order logic
Sonstige Titel: Resolutionsbasierte Entscheidungsverfahren für Teilklassen der Logik erster Stufe
Verfasser: Hustadt, Ullrich
Sprache: Englisch
Erscheinungsjahr: 1999
SWD-Schlagwörter: Terminologische Logik ; Modallogik ; Prädikatenlogik ; Stufe 1 ; Entscheidungsverfahren ; Resolution <Logik>
Freie Schlagwörter: Modallogik ; Automatisches Beweisverfahren
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: This thesis studies decidable fragments of first-order logic which are relevant to the field of nonclassical logic and knowledge representation. We show that refinements of resolution based on suitable liftable orderings provide decision procedures for the subclasses E+, K, and DK of first-order logic. By the use of semantics-based translation methods we can embed the description logic ALB and extensions of the basic modal logic K into fragments of first-order logic. We describe various decision procedures based on ordering refinements and selection functions for these fragments and show that a polynomial simulation of tableaux-based decision procedures for these logics is possible. In the final part of the thesis we develop a benchmark suite and perform an empirical analysis of various modal theorem provers.
Diese Arbeit untersucht entscheidbare Fragmente der Logik erster Stufe, die mit nicht-klassischen Logiken und Wissensrepräsentationsformalismen im Zusammenhang stehen. Wir zeigen, daß Entscheidungsverfahren für die Teilklassen E+, K, und DK der Logik erster Stufe unter Verwendung von Resolution eingeschränkt durch geeignete liftbare Ordnungen realisiert werden können. Durch Anwendung von semantikbasierten Übersetzungsverfahren lassen sich die Beschreibungslogik ALB und Erweiterungen der Basismodallogik K in Teilklassen der Logik erster Stufe einbetten. Wir stellen eine Reihe von Entscheidungsverfahren auf der Basis von Resolution eingeschränkt durch liftbare Ordnungen und Selektionsfunktionen für diese Logiken vor und zeigen, daß eine polynomielle Simulation von tableaux-basierten Entscheidungsverfahren für diese Logiken möglich ist. Im abschließenden Teil der Arbeit führen wir eine empirische Untersuchung der Performanz verschiedener modallogischer Theorembeweiser durch.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-1907
hdl:20.500.11880/25759
http://dx.doi.org/10.22028/D291-25703
Erstgutachter: Harald Ganzinger
Tag der mündlichen Prüfung: 8-Nov-1999
SciDok-Publikation: 6-Apr-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 
UllrichHustadt_ProfDrHaraldGanzinger.pdf1,98 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.