# Resolution with Order and Selection for Hybrid Logics

1 TALARIS - Natural Language Processing: representation, inference and semantics
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Keywords :
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2010, 46 (1), pp.1-42. 〈10.1007/s10817-010-9167-0〉

https://hal.inria.fr/inria-00519035
Contributeur : Areces Carlos <>
Soumis le : vendredi 17 septembre 2010 - 20:32:32
Dernière modification le : jeudi 11 janvier 2018 - 06:21:35

### Citation

Carlos Areces, Daniel Gorin. Resolution with Order and Selection for Hybrid Logics. Journal of Automated Reasoning, Springer Verlag, 2010, 46 (1), pp.1-42. 〈10.1007/s10817-010-9167-0〉. 〈inria-00519035〉

### Métriques

Consultations de la notice