Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment
Universität des Saarlandes, March, 2006
Magna Cum Laude
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 simplication 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.
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort
BibTeX Entry:
@PHDTHESIS{Kazakov2005,
AUTHOR = {Kazakov, Yevgeny},
TITLE = {Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2006},
TYPE = {Doctoral dissertation}
MONTH = {March},
NOTE = {Magna Cum Laude},
}