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

DOI10.1016/J.IC.2010.09.008MaRDI QIDQ764262zbMATH OpenOpenAlexFDO

Authors 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 eliminationKripke semanticssequent calculusconstructive linear-time temporal logic

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 1303434 (Why is no real title available?)
• scientific article; zbMATH DE number 1956524 (Why is no real title available?)
• scientific article; zbMATH DE number 1848312 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• scientific article; zbMATH DE number 970633 (Why is no real title available?)
• A Logical Foundation for Environment Classifiers
• A modal analysis of staged computation
• A polymorphic modal type system for Lisp-like multi-staged languages
• Computer Science Logic
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Constructive modal logics. I
• Environment classifiers
• Intuitionistic tense and modal logic
• MetaML and multi-stage programming with explicit annotations
• Modal logics with functional alternative relations
• Monad as modality
• Propositional lax logic
• Staged computation with names and necessity
• Structural cut elimination. I: Intuitionistic and classical logic

Cited in

(18)

• On a generalization of Heyting algebras. I
• scientific article; zbMATH DE number 1444739 (Why is no real title available?)
• Computer says no: verdict explainability for runtime monitors using a local proof system
• Combining linear-time temporal logic with constructiveness and paraconsistency
• Exploring the Jungle of Intuitionistic Temporal Logics
• A Paraconsistent Linear-time Temporal Logic
• A temporal logic approach to binding-time analysis
• Modality via iterated enrichment
• Parameter Synthesis for Timed Kripke Structures
• A Logical Foundation for Environment Classifiers
• A proof system for a unified temporal logic
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Intuitionistic -calculus with the Lewis arrow
• Cyclic Proofs for Linear Temporal Logic
• The intuitionistic temporal logic of dynamical systems
• Complete intuitionistic temporal logics for topological dynamics
• Ill-founded proof systems for intuitionistic linear-time temporal logic
• scientific article; zbMATH DE number 4170873 (Why is no real title available?)

Describes a project that uses

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)