On the Decidability of Intuitionistic Tense Logic without Disjunction

On the Decidability of Intuitionistic Tense Logic without Disjunction

Fei Liang, Zhe Lin

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence
Main track. Pages 1798-1804. https://doi.org/10.24963/ijcai.2020/249

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.
Keywords:
Knowledge Representation and Reasoning: Qualitative, Geometric, Spatial, Temporal Reasoning
Knowledge Representation and Reasoning: Non-monotonic Reasoning, Common-Sense Reasoning
Knowledge Representation and Reasoning: Other