inria-00519035, version 1
Resolution with Order and Selection for Hybrid Logics
Journal of Automated Reasoning 46, 1 (2010) 1-42
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.
- 1 :
- CNRS : UMR7503 – INRIA – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domaine : Informatique/Logique en informatique
- Mots-clés : Modal logic - Resolution calculus - Order and selection function constraints - Soundness and completeness - Termination
- inria-00519035, version 1
- http://hal.inria.fr/inria-00519035
- oai:hal.inria.fr:inria-00519035
- Contributeur :
- Soumis le : Vendredi 17 Septembre 2010, 20:32:32
- Dernière modification le : Mercredi 22 Juin 2011, 11:38:06




Documents associés
Exporter