A Hypersequent Calculus with Clusters for Data Logic over Ordinals - Laboratoire Méthodes Formelles Access content directly
Preprints, Working Papers, ... Year : 2019

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 hy-persequent system enriched with an ordering, clusters, and annotations. The proof system is tailored for proof search, and yields an optimal coNP complexity for validity and a small model property for our fragment.
Fichier principal
Vignette du fichier
main.pdf (497.71 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02165359 , version 1 (25-06-2019)

Identifiers

  • HAL Id : hal-02165359 , version 1

Cite

Anthony Lick. A Hypersequent Calculus with Clusters for Data Logic over Ordinals. 2019. ⟨hal-02165359⟩
61 View
110 Download

Share

Gmail Facebook X LinkedIn More