A Hypersequent Calculus with Clusters for Data Logic over Ordinals

Abstract

We study freeze tense logic over well-founded data streams. The logic features past- and future-navigating modalities along with freeze quantifiers, which store the datum of the current position and test data (in)equality later in the formula. We introduce a decidable fragment of that logic, and present a proof system that is sound for the whole logic, and complete for this fragment. Technically, this is a hypersequent system enriched with an ordering, clusters, and annotations. The proof system is tailored for proof search, and yields an optimal complexity for validity and a small model property for our fragment.