Hybrid Logic: Characterization, Interpolation and Complexity

Carlos Areces Patrick Blackburn 1 Maarten Marx
1 LANGUE ET DIALOGUE - Human-machine dialogue with a significant language component
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Hybrid languages are expansions of propositional modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to the work of Arthur Prior in the 1960s, but recent work has focussed on a more constrained system in which variables can only be bound to the current state. We show in detail that the constrained system is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fraisse game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result to emerge is that the constrained system corresponds to the fragment of first-order logic which is invariant for generated submodels. We then show that the system enjoys (strong) interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for an important subsystem called H(@). Finally, we provide complexity results for H(@) and other fragments and variants, and sharpen known undecidability results for the full fragment
Type de document :
Article dans une revue
The Journal of Symbolic Logic, Association for Symbolic Logic, 2001, 66 (3), pp.977-1010
Liste complète des métadonnées

Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:47:40
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48


  • HAL Id : inria-00100569, version 1



Carlos Areces, Patrick Blackburn, Maarten Marx. Hybrid Logic: Characterization, Interpolation and Complexity. The Journal of Symbolic Logic, Association for Symbolic Logic, 2001, 66 (3), pp.977-1010. 〈inria-00100569〉



Consultations de la notice