arXiv · 1803.05078
Bisimulations for intuitionistic temporal logics
Abstract
We introduce bisimulations for the logic $ITL^e$ with `next', `until' and `release', an intuitionistic temporal logic based on structures equipped with a partial order used to interpret intuitionistic implication and a monotone function used to interpret the temporal modalities. Our main results are that `eventually', which is definable in terms of `until', cannot be defined in terms of `next' and `henceforth', and similarly that `henceforth', definable in terms of `release', cannot be defined in terms of `next' and `until', even over the smaller class of here-and-there models.
Explore related subjects
Keep this discovery
Philippe Balbiani, Joseph Boudou, Marín Diéguez, David Fernández-Duque. 2018-03-14. Bisimulations for intuitionistic temporal logics. https://arxiv.org/abs/1803.05078
Cite the original work for its findings. Save a collection to share your selection of sources.