2026-07-21T12:18:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9914 2024-03-06T10:45:06Z ddc:004 open_access

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals Baelde, David Lick, Anthony Schmitz, Sylvain modal logic proof system hypersequent 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 omega^2. It also allows to answer the validity problem for ordinals below or exactly equal to a given one. Schloss Dagstuhl – Leibniz-Zentrum für Informatik David Baelde and Anthony Lick and Sylvain Schmitz 2018 Is Part Of LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2018.15 urn:nbn:de:0030-drops-99143 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.15 eng https://creativecommons.org/licenses/by/3.0/legalcode