Exploring the Jungle of Intuitionistic Temporal Logics. Issue 4 (22nd July 2021)

• Record Type: Journal Article
• Authors: BOUDOU, JOSEPH; DIÉGUEZ, MARTÍN; FERNÁNDEZ-DUQUE, DAVID; KREMER, PHILIP
• Is Part Of: Theory and practice of logic programming. Volume 21:Issue 4(2021)
• Page Start: 459
• Page End: 492
• Publication Date: 2021-07-22
• Subjects: Theory -- Knowledge Representation and Nonmonotonic Reasoning; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068421000089
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstract: The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible to extend functional programming languages with new features via type theory, while from the semantics perspective, several logics for reasoning about dynamical systems and several semantics for logic programming have their roots in this framework. We consider several axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. We provide two distinct interpretations of "henceforth", both of which are natural intuitionistic variants of the classical one. We completely establish the order relation between the semantically defined logics based on both interpretations of "henceforth" and, using our soundness results, show that the axiomatically defined logics enjoy the same order relations.