A Decidable Intuitionistic Temporal Logic

Authors Joseph Boudou, Martín Diéguez, David Fernández-Duque

Thumbnail PDF


  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Author Details

Joseph Boudou
Martín Diéguez
David Fernández-Duque

Cite AsGet BibTex

Joseph Boudou, Martín Diéguez, and David Fernández-Duque. A Decidable Intuitionistic Temporal Logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


We introduce the logic ITL^e, an intuitionistic temporal logic based on structures (W,R,S), where R is used to interpret intuitionistic implication and S is an R-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for ITL^e are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a 'persistent' version of the logic, ITL^p, whose models are similar to Cartesian products. We prove that, unlike ITL^e, ITL^p does not have the finite model property.
  • intuitionistic logic
  • temporal logic
  • products of modal logics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads