de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Hochschulschrift

Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44749

Kazakov,  Yevgeny
Programming Logics, MPI for Informatics, Max Planck Society;
International Max Planck Research School, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44730

Kapur,  Deepak
Programming Logics, MPI for Informatics, Max Planck Society;

Volltexte (frei zugänglich)

YevgenyThesis.pdf
(beliebiger Volltext), 3MB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Kazakov, Y. (2006). Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment. PhD Thesis, Universität des Saarlandes, Saarbrücken.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-21BA-8
Zusammenfassung
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.