Resolution with Order and Selection for Hybrid Logics - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Automated Reasoning Année : 2010

Resolution with Order and Selection for Hybrid Logics

Résumé

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 $\mathcal{H}(@,{\downarrow},\mathsf{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 $\mathcal{H}(@)$ 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.

Dates et versions

inria-00519035 , version 1 (17-09-2010)

Identifiants

Citer

Carlos Areces, Daniel Gorin. Resolution with Order and Selection for Hybrid Logics. Journal of Automated Reasoning, 2010, 46 (1), pp.1-42. ⟨10.1007/s10817-010-9167-0⟩. ⟨inria-00519035⟩
70 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More