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

DOI10.1016/J.IC.2010.09.008zbMATH Open1248.03031OpenAlexW2039659978MaRDI QIDQ764262FDOQ764262

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

Recommendations

• Combining linear-time temporal logic with constructiveness and paraconsistency
• Loop-type sequent calculi for temporal logic
• Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic
• Phase semantics for linear-time formalism
• Publication:4952320

zbMATH Keywords

cut eliminationKripke semanticssequent calculusconstructive linear-time temporal logic

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (14)

• Title not available (Why is that?)
• Exploring the Jungle of Intuitionistic Temporal Logics
• Computer says no: verdict explainability for runtime monitors using a local proof system
• A Paraconsistent Linear-time Temporal Logic
• Modality via iterated enrichment
• Parameter Synthesis for Timed Kripke Structures
• COMPLETE INTUITIONISTIC TEMPORAL LOGICS FOR TOPOLOGICAL DYNAMICS
• A Logical Foundation for Environment Classifiers
• A proof system for a unified temporal logic
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Cyclic Proofs for Linear Temporal Logic
• The intuitionistic temporal logic of dynamical systems
• Ill-founded proof systems for intuitionistic linear-time temporal logic
• Title not available (Why is that?)

Uses Software

• MiniML

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

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