English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment

MPS-Authors
/persons/resource/persons44749

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

Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

YevgenyThesis.pdf
(Any fulltext), 3MB

Supplementary Material (public)
There is no public supplementary material available
Citation

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


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