arXiv · 1704.02847
A Decidable Intuitionistic Temporal Logic
Abstract
We introduce the logic $\sf ITL^e$, an intuitionistic temporal logic based on structures $(W,\preccurlyeq,S)$, where $\preccurlyeq$ is used to interpret intuitionistic implication and $S$ is a $\preccurlyeq$-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for $\sf 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, $\sf ITL^p$, whose models are similar to Cartesian products. We prove that, unlike $\sf ITL^e$, $\sf ITL^p$ does not have the finite model property.
Explore related subjects
Keep this discovery
Joseph Boudou, Martín Diéguez, David Fernández-Duque. 2017-04-10. A Decidable Intuitionistic Temporal Logic. https://arxiv.org/abs/1704.02847
Cite the original work for its findings. Save a collection to share your selection of sources.