Cyclic Proofs for Linear Temporal Logic

DOI10.1515/9781501502620-011MaRDI QIDQ5221853zbMATH OpenOpenAlexFDO

Authors Ioannis Kokkinis, Thomas Studer

Publication date 3 April 2020

Published in Concepts of Proof in Mathematics, Philosophy, and Computer Science (Search for Journal in Brave)

Full work available at URL https://boris.unibe.ch/85668/1/ks16.pdf

zbMATH Keywords

proof theorytemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Recommendations

• Proving linearizability with temporal logic
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• The axiomatization of propositional linear time temporal logic
• An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
• The temporal logic of linear time frames with inductions axiom
• Bounded linear-time temporal logic: a proof-theoretic investigation
• The complexity of propositional linear temporal logics
• Loop-type sequent calculi for temporal logic
• Intuitionistic linear temporal logics

Cited in

(10)

• Loop-check specification for a sequent calculus of temporal logic
• Uniform interpolation from cyclic proofs: the case of modal mu-calculus
• Loop-type sequent calculi for temporal logic
• The proof theory of common knowledge
• More efficient proof-search for sequents of temporal logic
• Cyclic hypersequent system for transitive closure logic
• Ill-founded proof systems for intuitionistic linear-time temporal logic
• Loop-check free sequent calculi for unary fragment of temporal logic
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
• Global condition check strategy for a cyclic sequent calculus of temporal logic

This page was built for publication: Cyclic Proofs for Linear Temporal Logic

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