Cut-free sequent systems for temporal logic

DOI10.1016/j.jlap.2008.02.004zbMath1151.03009OpenAlexW2047456744MaRDI QIDQ941433

Martin Lange, Kai Brünnler

Publication date: 1 September 2008

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://boris.unibe.ch/37186/1/bl08.pdf

zbMATH Keywords

temporal logicLTLCTLcut-free sequent calculusfocus games

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44)

Related Items (16)

Completeness and decidability results for CTL in constructive type theory ⋮ Cyclic hypersequent calculi for some modal logics with the master modality ⋮ More efficient proof-search for sequents of temporal logic ⋮ Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic ⋮ Unnamed Item ⋮ Loop-type sequent calculi for temporal logic ⋮ The Proof Theory of Common Knowledge ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\) ⋮ Computer says no: verdict explainability for runtime monitors using a local proof system ⋮ An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability ⋮ On the proof theory of the modal mu-calculus ⋮ Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach ⋮ Dual systems of tableaux and sequents for PLTL ⋮ Loop-check specification for a sequent calculus of temporal logic ⋮ A goal-directed decision procedure for hybrid PDL

Uses Software

• TTM

Cites Work

• Results on the propositional \(\mu\)-calculus
• Propositional dynamic logic of regular programs
• Cut-free common knowledge
• Deduction chains for common knowledge
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• Sequential Calculus for a First Order Infinitary Temporal Logic
• Propositional temporal logics: decidability and completeness
• Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus
• KI 2003: Advances in Artificial Intelligence
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Cut-free sequent systems for temporal logic