Saturation−Based Decision Procedures for Extensions of the Guarded Fragment
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 <em>EL</em>, which allows for conjunction and existential restrictions only, and ending wi...
| Main Author: | |
|---|---|
| Format: | Thesis |
| Published: |
Saarbrücken‚ Germany
2006
|