Syntactic cut-elimination for a fragment of the modal mu-calculus

DOI10.1016/j.apal.2012.04.006zbMath1259.03031OpenAlexW2020453924MaRDI QIDQ714717

Thomas Studer, Kai Brünnler

Publication date: 11 October 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2012.04.006

zbMATH Keywords

cut eliminationmu-calculusnested sequentsinfinitary sequent system

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Related Items (3)

Intuitionistic common knowledge or belief ⋮ The Proof Theory of Common Knowledge ⋮ SMALL INFINITARY EPISTEMIC LOGICS

Cites Work

• Games for the \(\mu\)-calculus
• Results on the propositional \(\mu\)-calculus
• Canonical completeness of infinitary \(\mu \)
• A contraction-free and cut-free sequent calculus for propositional dynamic logic
• Syntactic cut-elimination for common knowledge
• A finite model theorem for the propositional \(\mu\)-calculus
• Cut-free sequent calculi for some tense logics
• Proof theory. An introduction
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Cut elimination for a logic with induction and co-induction
• The variable hierarchy of the \(\mu\)-calculus is strict
• Continuous Fragment of the mu-Calculus
• The Method of Tree-Hypersequents for Modal Propositional Logic
• Syntactic Cut-elimination for Common Knowledge
• Least and Greatest Fixed Points in Linear Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Syntactic cut-elimination for a fragment of the modal mu-calculus