On the proof theory of the modal mu-calculus

DOI10.1007/s11225-008-9133-6zbMath1163.03014OpenAlexW2081909835MaRDI QIDQ1005937

Thomas Studer

Publication date: 17 March 2009

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://boris.unibe.ch/37094/1/stu08.pdf

zbMATH Keywords

finite model propertymodal \(\mu\)-calculusinfinitary proofsproof translation

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Relative consistency and interpretations (03F25)

Related Items

A focus system for the alternation-free \(\mu \)-calculus ⋮ $\aleph_1$ and the modal $\mu$-calculus ⋮ Two Ways to Common Knowledge ⋮ Unnamed Item ⋮ Semirings of Evidence ⋮ Cyclic hypersequent system for transitive closure logic ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Cyclic Arithmetic Is Equivalent to Peano Arithmetic ⋮ Cyclic proofs, hypersequents, and transitive closure logic

Uses Software

• TTM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Games for the \(\mu\)-calculus
• Results on the propositional \(\mu\)-calculus
• Cut-free sequent systems for temporal logic
• Canonical completeness of infinitary \(\mu \)
• A finite model theorem for the propositional \(\mu\)-calculus
• Propositional dynamic logic of regular programs
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Cut-free common knowledge
• Sequent calculi for induction and infinite descent
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• The Complexity of Tree Automata and Logics of Programs
• Syntactic Cut-elimination for Common Knowledge
• A Proof System for the Linear Time μ-Calculus

This page was built for publication: On the proof theory of the modal mu-calculus