文档介绍：SATURATION-BASED DECISION PROCEDURES
FOR
EXTENSIONS OF THE GUARDED FRAGMENT
Dissertation
zur Erlangung des Grades
Doktor der Ingenieurwissenschaften (Dr.-Ing.)
der Naturwissenschaftlich-Technischen Fakultät I
der Universität des Saarlandes
von
Yevgeny Kazakov
Saarbrücken
2005
Verfasser: Yevgeny Kazakov
Max-Planck Institut für Informatik
Stuhlsatzenhausweg 85
66123 Saarbrücken
Germany
******@mpi-
Dekan: Prof. Dr. Jörg Eschmeier
Prüfungsausschuss: Prof. Dr. Jörg Siekmann
Prof. Dr. Franz Baader
Prof. Dr. Gert Smolka
Dr. Hans de Nivelle
Dr. Uwe Waldman
Tag des Kolloquiums:
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 exis-
tential restrictions only, and ending with extensions of the guarded fragment with
equality, constants, functionality, number restrictions positional 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 no-
tion 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-plexity and
direct correctness proofs.
ZUSAMMENFASSUNG
Wir wenden das Framework von Bachmair und Ganzinger für saturierungsbasiertes
Theorembeweisen an, um eine Reihe von Entscheidungsverfahren für logische For-
malismen 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, Zahlenrestrik-
tionen und Kompositionsaxiomen der Form S ◦ T ⊆ H. Unsere Verfaren sind ein-
heitlich abge