On the Decidability of Intuitionistic Tense Logic Without Disjunction
Abstract
Implicative semi-lattices (also known as Brouwerian semi-lattices) are a generalization of Heyting algebras, and have been already well studied both from a logical and an algebraic perspective. In this paper, we consider the variety ISt of the expansions of implicative semi-lattices with tense modal operators, which are algebraic models of the disjunction-free fragment of intuitionistic tense logic. Using methods from algebraic proof theory, we show that the logic of tense implicative semi-lattices has the finite model property. Combining with the finite axiomatizability of the logic, it follows that the logic is decidable.
Cite
Text
Liang and Lin. "On the Decidability of Intuitionistic Tense Logic Without Disjunction." International Joint Conference on Artificial Intelligence, 2020. doi:10.24963/IJCAI.2020/249Markdown
[Liang and Lin. "On the Decidability of Intuitionistic Tense Logic Without Disjunction." International Joint Conference on Artificial Intelligence, 2020.](https://mlanthology.org/ijcai/2020/liang2020ijcai-decidability/) doi:10.24963/IJCAI.2020/249BibTeX
@inproceedings{liang2020ijcai-decidability,
title = {{On the Decidability of Intuitionistic Tense Logic Without Disjunction}},
author = {Liang, Fei and Lin, Zhe},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2020},
pages = {1798-1804},
doi = {10.24963/IJCAI.2020/249},
url = {https://mlanthology.org/ijcai/2020/liang2020ijcai-decidability/}
}