@InCollection{Areces2001e,
  author =       "C. Areces and P. Blackburn and M. Marx",
  booktitle =    "Proceedings of the 16th Annual IEEE Symp.\ on Logic in
                 Computer Science, {LICS} 2001",
  title =        "Repairing the Interpolation Theorem in First-Order
                 Modal Logic",
  year =         "2001",
  abstract =     "Hybrid logics are extensions of orthodox modal logics
                 in which it is possible to name worlds (or states, or
                 times, ...). Such extensions have proved interesting
                 for a number of reasons. We often want to reason about
                 what happens at particular states, times, or locations,
                 and this isn’t possible in orthodox modal logics. In
                 addition, hybridization can improve the behavior of the
                 underlying modal logic. For example, many modally
                 undefinable properties (such as irreflexivity) are
                 definable in hybrid logic, and general completeness and
                 interpolation results can be obtained. Previous work
                 has examined the effects of hybridizing propositional
                 modal logics. But what happens when a first-order modal
                 logic is hybridized? First-order modal logics are often
                 badly behaved — does hybridization improve the
                 situation? As far as interpolation is concerned, yes.
                 As we shall see, hybridization allows us to repair
                 failures of interpolation in first-order modal logic,
                 in a very general way. This abstract is not self
                 contained. For first-order modal logic (and in
                 particular, a discussion of varying, expanding,
                 contracting, and constant domains), see Fitting and
                 Mendelsohn [4]. For Beth definability and Craig
                 iterpolation, see Chang and Keisler [2]. As for hybrid
                 logic, the most relevant points are the following.
                 Hybrid logic contains special variables, written w, w0
                 , . . . , which range over worlds. Prefixing a formula
                 by ↓w binds the variable w to the world of
                 evaluation, while prefixing a formula by @w means that
                 the formula should be evaluated at the state named by
                 w. As the examples below show, it is the interplay
                 between ↓w (“let w name the current state”) and
                 @w (“evaluate at the state named by w”) that enable
                 us to create interpolants so easily. For a detailed
                 examination of \downarrow and @ in the propositional
                 case, see Areces, Blackburn and Marx [1].",
  editor =       "J. Halpern",
  note =         "Short Presentation",
  publisher =    "IEEE Computer Society Press",
  ISBN =         "978-0-7695-1281-5",
}