Resolution with order and selection for hybrid logics
We investigate labeled resolution calculi for hybrid logics with inference rules restricted via selection functions and orders. We start by providing a sound and refutationally complete calculus for the hybrid logic H(at ↓,A), even under restrictions by selection functions and orders. Then, by impos...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_01687433_v46_n1_p1_Areces |
| Aporte de: |
| Sumario: | We investigate labeled resolution calculi for hybrid logics with inference rules restricted via selection functions and orders. We start by providing a sound and refutationally complete calculus for the hybrid logic H(at ↓,A), even under restrictions by selection functions and orders. Then, by imposing further restrictions in the original calculus, we develop a sound, complete and terminating calculus for the H(at) sublanguage. The proof scheme we use to show refutational completeness of these calculi is an adaptation of a standard completeness proof for saturation-based calculi for first-order logic that guarantees completeness even under redundancy elimination. In fact, one of the contributions of this article is to show that the general framework of saturation-based proving for first-order logic with equality can be naturally adapted to saturation-based calculi for other languages, in particular modal and hybrid logics. © 2010 Springer Science+Business Media B.V. |
|---|