A Decidable Intuitionistic Temporal Logic

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

We introduce the logic $\mathsf{IT}{\mathsf{L}}^{\mathsf{e}}$, an intuitionistic temporal logic based on structures $(W,\preccurlyeq ,S)$, where $\preccurlyeq$ is used to interpret intuitionistic implication…