Constructive linear-time temporal logic: proof systems and Kripke semantics

DOI10.1016/J.IC.2010.09.008zbMath1248.03031OpenAlexW2039659978MaRDI QIDQ764262

Kensuke Kojima, Atsushi Igarashi

Publication date: 13 March 2012

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2010.09.008

zbMATH Keywords

cut eliminationsequent calculusKripke semanticsconstructive linear-time temporal logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44)

Related Items (7)

Modality via iterated enrichment ⋮ COMPLETE INTUITIONISTIC TEMPORAL LOGICS FOR TOPOLOGICAL DYNAMICS ⋮ Exploring the Jungle of Intuitionistic Temporal Logics ⋮ Computer says no: verdict explainability for runtime monitors using a local proof system ⋮ The intuitionistic temporal logic of dynamical systems ⋮ A Logical Foundation for Environment Classifiers ⋮ Constructive linear-time temporal logic: proof systems and Kripke semantics

Uses Software

• MiniML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructive modal logics. I
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Modal logics with functional alternative relations
• Propositional lax logic
• Monad as modality
• MetaML and multi-stage programming with explicit annotations
• Structural cut elimination. I: Intuitionistic and classical logic
• Environment classifiers
• A modal analysis of staged computation
• Intuitionistic tense and modal logic
• Computer Science Logic
• A polymorphic modal type system for lisp-like multi-staged languages
• Staged computation with names and necessity
• A Logical Foundation for Environment Classifiers

This page was built for publication: Constructive linear-time temporal logic: proof systems and Kripke semantics