A Decidable Intuitionistic Temporal Logic

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



PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.14.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)
https://doi.org/10.4230/LIPIcs.CSL.2017.14

Abstract

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.
Keywords
  • intuitionistic logic
  • temporal logic
  • products of modal logics

Metrics

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