Constructive Interpolation in Hybrid Logic
Patrick Blackburn, Maarten Marx

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 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 its 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.