2026-07-20T07:29:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7701 2024-03-06T10:40:44Z ddc:004 open_access

A Decidable Intuitionistic Temporal Logic Boudou, Joseph Diéguez, Martín Fernández-Duque, David intuitionistic logic temporal logic products of modal logics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Joseph Boudou and Martín Diéguez and David Fernández-Duque 2017 Is Part Of LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2017.14 urn:nbn:de:0030-drops-77016 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.14 eng https://creativecommons.org/licenses/by/3.0/legalcode