Intuitionistic linear temporal logics

DOI10.1145/3365833MaRDI QIDQ5216145zbMATH OpenOpenAlexWikidataFDO

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

Publication date 14 February 2020

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1912.12893, https://oatao.univ-toulouse.fr/26276/1/balbiani_26276.pdf

zbMATH Keywords

bisimulationintuitionistic logicmathematics of computingtemporal logictheory of computation

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Abstract: We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on expanding posets: partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic which we denote $iltl$, and by imposing additional constraints we obtain the logics $itlb$ of persistent posets and $itlht$ of here-and-there temporal logic, both of which have been considered in the literature. We prove that $iltl$ has the effective finite model property and hence is decidable, while $itlb$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the `until' and `release' operators are not definable in terms of each other, even over the class of persistent posets.

Recommendations

• Bisimulations for intuitionistic temporal logics
• A decidable intuitionistic temporal logic
• An intuitionistic axiomatization of `eventually'
• Complete intuitionistic temporal logics for topological dynamics
• Combining linear-time temporal logic with constructiveness and paraconsistency

Cited in

(30)

• Linear, branching time and joint closure semantics for temporal logic
• On the finite model property of weak intuitionistic tense logic
• Axiomatic systems and topological semantics for intuitionistic temporal logic
• Linear and affine logics with temporal, spatial and epistemic operators
• The temporal logic of linear time frames with inductions axiom
• Polymodal logic of the class of inductive linear time frames
• A Paraconsistent Linear-time Temporal Logic
• Logical Consecutions in Intransitive Temporal Linear Logic of Finite Intervals
• Intuitionistic linear-time -calculus
• The intuitionistic temporal logic of dynamical systems
• Bisimulations for intuitionistic temporal logics
• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
• Complete intuitionistic temporal logics for topological dynamics
• A decidable intuitionistic temporal logic
• A strongly complete axiomatization of intuitionistic temporal logic
• Cyclic Proofs for Linear Temporal Logic
• An intuitionistic axiomatization of `eventually'
• Computer Science Logic
• Algebraic Methodology and Software Technology
• Interval Temporal Logic Semantics of Box Algebra
• Logical consecutions in discrete linear temporal logic
• An algebraic study of tense logics with linear time
• Exploring the Jungle of Intuitionistic Temporal Logics
• Time and Gödel: fuzzy temporal reasoning in PSPACE
• Ill-founded proof systems for intuitionistic linear-time temporal logic
• Gödel-Dummett linear temporal logic
• Intuitionistic -calculus with the Lewis arrow
• Multi-succedent sequent calculus for intuitionistic epistemic logic
• Linear-time temporal answer set programming
• Unification in linear temporal logic LTL

This page was built for publication: Intuitionistic linear temporal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5216145)