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: |
| id |
todo:paper_01687433_v46_n1_p1_Areces |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_01687433_v46_n1_p1_Areces2023-10-03T15:06:38Z Resolution with order and selection for hybrid logics Areces, C. Gorín, D. Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Biomineralization Formal logic Pathology Calculations 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. Fil:Areces, C. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Gorín, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_01687433_v46_n1_p1_Areces |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Biomineralization Formal logic Pathology Calculations |
| spellingShingle |
Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Biomineralization Formal logic Pathology Calculations Areces, C. Gorín, D. Resolution with order and selection for hybrid logics |
| topic_facet |
Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Modal logic Order and selection function constraints Resolution calculus Soundness and completeness Termination Biomineralization Formal logic Pathology Calculations |
| description |
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. |
| format |
JOUR |
| author |
Areces, C. Gorín, D. |
| author_facet |
Areces, C. Gorín, D. |
| author_sort |
Areces, C. |
| title |
Resolution with order and selection for hybrid logics |
| title_short |
Resolution with order and selection for hybrid logics |
| title_full |
Resolution with order and selection for hybrid logics |
| title_fullStr |
Resolution with order and selection for hybrid logics |
| title_full_unstemmed |
Resolution with order and selection for hybrid logics |
| title_sort |
resolution with order and selection for hybrid logics |
| url |
http://hdl.handle.net/20.500.12110/paper_01687433_v46_n1_p1_Areces |
| work_keys_str_mv |
AT arecesc resolutionwithorderandselectionforhybridlogics AT gorind resolutionwithorderandselectionforhybridlogics |
| _version_ |
1807323172032217088 |