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.
Type de document :
Communication dans un congrès
Sumit Ganguly and Paritosh Pandya. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018, Ahmedabad, India. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 122, pp.15:1--15:19, Leibniz International Proceedings in Informatics. 〈10.4230/LIPIcs.FSTTCS.2018.15〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01852077
Contributeur : Sylvain Schmitz <>
Soumis le : jeudi 13 décembre 2018 - 13:28:56
Dernière modification le : vendredi 14 décembre 2018 - 01:17:31

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Partage selon les Conditions Initiales 4.0 International License

Identifiants

Collections

Citation

David Baelde, Anthony Lick, Sylvain Schmitz. A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. Sumit Ganguly and Paritosh Pandya. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018, Ahmedabad, India. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 122, pp.15:1--15:19, Leibniz International Proceedings in Informatics. 〈10.4230/LIPIcs.FSTTCS.2018.15〉. 〈hal-01852077v2〉

Partager

Métriques

Consultations de la notice

2

Téléchargements de fichiers

1