A Hypersequent Calculus with Clusters for Tense Logic over Ordinals

Abstract : Prior's tense logic forms the core of linear temporal logic, with both past-and future-looking modalities. We present a sound and complete proof system for tense logic over ordinals. Technically , this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem. It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most ω². It also allows to answer the validity problem for ordinals below or exactly equal to a given one.
Document type :
Conference papers
Complete list of metadatas

Cited literature [40 references]  Display  Hide  Download

https://hal.inria.fr/hal-01852077
Contributor : Sylvain Schmitz <>
Submitted on : Thursday, December 13, 2018 - 1:28:56 PM
Last modification on : Wednesday, October 2, 2019 - 4:32:08 PM
Long-term archiving on : Thursday, March 14, 2019 - 2:25:07 PM

File

main.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License

Identifiers

Citation

David Baelde, Anthony Lick, Sylvain Schmitz. A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. FSTTCS 2018 - 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2018, Ahmedabad, India. pp.15:1--15:19, ⟨10.4230/LIPIcs.FSTTCS.2018.15⟩. ⟨hal-01852077v2⟩

Share

Metrics

Record views

74

Files downloads

162