Selected publications at LSV

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 ω2. It also allows to answer the validity problem for ordinals below or exactly equal to a given one.

   address = {Ahmedabad, India},
   author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain},
   booktitle = {{P}roceedings of the 38th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'18)},
   DOI = {10.4230/LIPIcs.FSTTCS.2018.15},
   editor = {Sumit Ganguly and Paritosh Pandya},
   month = dec,
   pages = {15:1-15:19},
   publisher = {Leibniz-Zentrum f{\"u}r Informatik},
   series = {Leibniz International Proceedings in Informatics},
   title = {A Hypersequent Calculus with Clusters for Tense Logic over Ordinals},
   url = {},
   year = {2018},

About LSV

Select by Year