Hybrid logics: Characterization, interpolation and complexity

Carlos Areces*, Patrick Blackburn, Maarten Marx

*Corresponding author

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Abstract

Hybrid languages are expansions of prepositional 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, BT98a, BT99]) has focussed on a more constrained system called ℋ(↓,commercial at). We show in detail that ℋ(↓, commercial at) is modally natural. We begin by studying its expressivity, and provide 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 to emerge is that ℋ(↓, commercial at) corresponds to the fragment of first-order logic which is invariant for generated submodels. We then show that ℋ (↓, commercial at) enjoys (strong) interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage ℋ(commercial at). Finally, we provide complexity results for ℋ(commercial at) and other fragments and variants, and sharpen known undecidability results for ℋ(↓, commercial at).
OriginalsprogEngelsk
TidsskriftJournal of Symbolic Logic
Vol/bind66
Udgave nummer3
Sider (fra-til)977-1010
Antal sider34
ISSN0022-4812
DOI
StatusUdgivet - sep. 2001
Udgivet eksterntJa

Citer dette