Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-25736
Titel: | Optimised modal translation and resolution |
VerfasserIn: | Schmidt, Renate A. |
Sprache: | Englisch |
Erscheinungsjahr: | 1997 |
Kontrollierte Schlagwörter: | Modallogik ; Klausellogik ; Funktionale Semantik ; Theorieresolution |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Dissertation |
Abstract: | This thesis studies the optimised functional translation of propositional modal logics to first-order logic, and first-order resolution as a means for realising modal reasoning. The optimised functional translation maps modal logics to a lattice of clausal logics, called path logics. The general apparatus of inference for path logics is theory resolution. We show that satisfiability in basic path logic and certain extensions can be decided by resolution and condensing without requiring additional refinement strategies. We propose an improved theory unification algorithm for S4, and we present a calculus of ordered E-resolution with normalisation. We show also that some essentially second-order modal logics convert to path logics, which can be exploited for accomodating inference for modal logics with numerical quantifiers in a calculus of resolution and simple arithmetic. Diese Arbeit untersucht die optimierte funktionale Übersetzung von modalen Aussagelogiken in die Prädikatenlogik erster Stufe und deren Behandlung durch Resolutionsverfahren. Die optimierte funktionale Übersetzung bildet Modallogiken in Klausellogiken, genannt Pfadlogiken, ab. Der allgemeine Interferenzformalismus für Pfadlogiken ist Theorieresolution. Wir zeigen, Resolution und Kondensierung ohne zusätzliche Verfeinerungsstrategien ist ein Entscheidungsverfahren für die Basispfadlogik und bestimmte Erweiterungen. Wir präsentieren einen verbesserten Theorieunifikationsalgorithmus für die Logik S4, sowie ein geordnetes E-Resolutionskalkül mit Normalisierungsfunktionen. Wir zeigen ausserdem, dass die optimierte funktionale Übersetzung auch auf Axiomenschemas anwendbar ist. Dies ermöglicht insbesondere die Einbettung von Modallogiken mit Zählquantoren in die Logik erster Stufe und deren Behandlung mittels eines Kalküls, das Resolution und Arithmetik verbindet. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291-scidok-2288 hdl:20.500.11880/25792 http://dx.doi.org/10.22028/D291-25736 |
Erstgutachter: | Hans Jürgen Ohlbach |
Tag der mündlichen Prüfung: | 3-Nov-1997 |
Datum des Eintrags: | 10-Mai-2004 |
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öße | Format | |
---|---|---|---|---|
RenateSchmidt_ProfDrHansJuergenOhlbach.pdf | 2,15 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.