Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-25860
Titel: | Saturation-based decision procedures for extensions of the guarded fragment |
VerfasserIn: | Kazakov, Yevgeny |
Sprache: | Englisch |
Erscheinungsjahr: | 2005 |
Kontrollierte Schlagwörter: | Entscheidungsverfahren Automatisches Beweisverfahren Terminologische Logik |
Freie Schlagwörter: | saturierungsbasiertes Theorembeweisen Korrektheitsbeweis Beschreibungslogik saturation-based theorem proving decision procedure correctness proof guarded fragment |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Dissertation |
Abstract: | We apply the framework of Bachmair and Ganzinger for saturation-based theorem proving to derive a range of decision procedures for logical formalisms, starting with a simple terminological language EL, which allows for conjunction and existential restrictions only, and ending with extensions of the guarded fragment with equality, constants, functionality, number restrictions and compositional axioms of form S ◦ T ⊆ H. Our procedures are derived in a uniform way using standard saturation-based calculi enhanced with simplification rules based on the general notion of redundancy. We argue that such decision procedures can be applied for reasoning in expressive description logics, where they have certain advantages over traditionally used tableau procedures, such as optimal worst-case complexity and direct correctness proofs. Wir wenden das Framework von Bachmair und Ganzinger für saturierungsbasiertes Theorembeweisen an, um eine Reihe von Entscheidungsverfahren für logische Formalismen abzuleiten, angefangen von einer simplen terminologischen Sprache EL, die nur Konjunktionen und existentielle Restriktionen erlaubt, bis zu Erweiterungen des Guarded Fragment mit Gleichheit, Konstanten, Funktionalität, Zahlenrestriktionen und Kompositionsaxiomen der Form S ◦ T ⊆ H. Unsere Verfahren sind einheitlich abgeleitet unter Benutzung herkömmlicher saturierungsbasierter Kalküle, verbessert durch Simplifikationsregeln, die auf dem Konzept der Redundanz basieren. Wir argumentieren, daß solche Entscheidungsprozeduren für das Beweisen in ausdrucksvollen Beschreibungslogiken angewendet werden können, wo sie gewisse Vorteile gegenüber traditionell benutzten Tableauverfahren besitzen, wie z.B. optimale worst-case Komplexität und direkte Korrektheitsbeweise. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291-scidok-11373 hdl:20.500.11880/25916 http://dx.doi.org/10.22028/D291-25860 |
Erstgutachter: | Siekmann, Jörg |
Tag der mündlichen Prüfung: | 17-Mär-2006 |
Datum des Eintrags: | 31-Mai-2007 |
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 | |
---|---|---|---|---|
Dissertation_691_Kaza_Yevg_2005.pdf | 3,05 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.