| Summary: | We study a family of modal logics interpreted on tree-like structures, and featuring local quantifiers ∃kp that bind the proposition p to worlds that are accessible from the current one in at most k steps. We consider a first-order and a second-order semantics for the quantifiers, which enables us to relate several well-known formalisms, such as hybrid logics, S5Q and graded modal logic. To better stress these connections, we explore fragments of our logics, called herein round-bounded fragments. Depending on whether first or second-order semantics is considered, these fragments populate the hierarchy 2NEXP⊂3NEXP⊂⋯ or the hierarchy 2AEXPpol⊂3AEXPpol⊂⋯, respectively. For formulae up-to modal depth k, the complexity improves by one exponential.
|
|---|