Hybrid logic is the bounded fragment of first order logic

C. Areces, P. Blackburn, and M. Marx. Hybrid logic is the bounded fragment of first order logic. In Proceedings of 6th Workshop on Logic, Language, Information and Computation, WOLLIC99, pp. 33–50, Rio de Janeiro, Brazil, 1999.

Download

[pdf] 

Abstract

Hybrid languages are extended modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work (for example [BS98, BT99]) has focussed on a more constrained system called H(\downarrow, @). The purpose of the present paper is to show in detail that H(\dowarrow, @) is a modally natural system. We study its expressivity, and provide both model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fraı̈ssé game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result is that H(\downarrow, @) corresponds precisely to the first-order fragment which is invariant for generated submodels.

BibTeX

@InProceedings{Areces1999c,
  author =       "C. Areces and P. Blackburn and M. Marx",
  booktitle =    "Proceedings of 6th Workshop on Logic, Language,
                 Information and Computation, WOLLIC99",
  title =        "Hybrid logic is the bounded fragment of first order
                 logic",
  year =         "1999",
  abstract =     "Hybrid languages are extended modal languages which
                 can refer to (or even quantify over) worlds. The use of
                 strong hybrid languages dates back to at least [Pri67],
                 but recent work (for example [BS98, BT99]) has focussed
                 on a more constrained system called H(\downarrow, @).
                 The purpose of the present paper is to show in detail
                 that H(\dowarrow, @) is a modally natural system. We
                 study its expressivity, and provide both model
                 theoretic characterizations (via a restricted notion of
                 Ehrenfeucht-Fraı̈ssé game, and an enriched notion of
                 bisimulation) and a syntactic characterization (in
                 terms of bounded formulas). The key result is that
                 H(\downarrow, @) corresponds precisely to the
                 first-order fragment which is invariant for generated
                 submodels.",
  address =      "Rio de Janeiro, Brazil",
  editor =       "R. de Queiroz and W. Carnielli",
  pages =        "33--50",
}