LIPIcs.CSL.2017.14.pdf
- Filesize: 0.55 MB
- 17 pages
Document
A Decidable Intuitionistic Temporal Logic
Authors
-
Part of:
Volume:
26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-16
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
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)
0PDF Downloads