Craig’s interpolation lemma (if $φ\rightarrowψ$ is valid, then
$φ\rightarrowθ$ and $θ\rightarrowψ$ are valid, for
θ a formula constructed using only primitive symbols which
occur both in φ and ψ) 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.