Thesis icon

Thesis

Saturation−Based Decision Procedures for Extensions of the Guarded Fragment

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\\circ T< H. Our procedures are derived in a uniform way using standard s...

Expand abstract

Actions


Authors


Publisher:
Saarbrücken‚ Germany
Publication date:
2006-03-01
UUID:
uuid:8e78dca2-1518-4660-a140-e7abd436cd16
Local pid:
cs:876
Deposit date:
2015-03-31

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP