Constructive Interpolation in Hybrid Logic

Patrick Blackburn 1 Maarten Marx 2
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 : Craig's interpolation lemma fails for many propositional and first order modal logics. The interpolation property is often regarded as a sign of well-matched syntax and semantics. Hybrid logicians claim that orthodox modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such machinery solves many technical problems. The paper presents strong evidence for this claim by defining interpolation algorithms for both propositional and first order hybrid logic. These algorithms produce interpolants for the hybrid logic of every elementary class of frames satisfying the property that a frame is in the class if and only if all itsc point-generated subframes are in the class. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it computes interpolants in which the hybrid syntactic machinery does not occur.
Type de document :
Article dans une revue
The Journal of Symbolic Logic, Association for Symbolic Logic, 2003, 68 (2), pp.463-480
Liste complète des métadonnées
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:39:38
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48


  • HAL Id : inria-00099632, version 1



Patrick Blackburn, Maarten Marx. Constructive Interpolation in Hybrid Logic. The Journal of Symbolic Logic, Association for Symbolic Logic, 2003, 68 (2), pp.463-480. 〈inria-00099632〉



Consultations de la notice