Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template :: Thesis :: Kazakov, Yevgeny


Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit


Author
Author(s)*:Kazakov, Yevgeny
BibTeX citekey*:Kazakov2005
Language:English

Title, School
Title*:Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation
Month:March
Year:2006


Note, Abstract, Copyright
Note:Magna Cum Laude
LaTeX 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 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.

Download Access Level:Public
Download File(s):View attachments here:

Referees, Status, Dates
1. Referee:Prof. Dr. rer. nat. Gert Smolka
2. Referee:Prof. Dr.-Ing. Franz Baader
Supervisor:Dr.-Ing. Hans de Nivelle
Status:Completed
Location of Lecture:MPI R024
Date Kolloquium:17 March 2006

Correlation
MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:Expert
Appearance: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},
}


Hide details for Attachment SectionAttachment Section
YevgenyThesis.pdf
View attachments here:




Entry last modified by Uwe Brahm, 03/16/2013
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Veronika Weinand
Created
04/03/2006 02:46:43 PM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm
Veronika Weinand
Veronika Weinand
Edit Dates
16-03-2013 12:16:09 PM
04/10/2007 07:25:44 PM
04/10/2007 07:24:20 PM
24.01.2007 11:44:43
03.04.2006 16:02:46