On the proof theory of the modal mu-calculus
type: Item
instance of: scholarly article
title: On the proof theory of the modal mu-calculus
zbMATH Open document ID: 1163.03014
author: Thomas Studer
published in: Studia Logica
publication date: 2009-03-17T00:00:00Z
full work available at URL: stu08.pdf
review text: The paper investigates two cut-free infinitary deduction systems for the modal \(\mu\)-calculus. The first one is the system \(T^\omega_{\mu+}\), introduced by \textit{G. Jäger, M. Kretz} and \textit{T. Studer} [J. Log. Algebr. Program. 76, No.~2, 270--292 (2008; Zbl 1156.68013)], which includes a variant of an infinitary \(\omega\)-rule. The second one is \(T^{\text{pre}}_\mu\), which is an adaptation to modal \(\mu\)-calculus of a proof system by \textit{C. Dax, M. Hofmann} and \textit{M. Lange} [Lect. Notes Comput. Sci. 4337, 273--284 (2006; Zbl 1163.03308)] for the linear-time \(\mu\)-calculus; it has finitary rules, but allows infinite branches in proof trees under certain conditions. The main result of the paper is a translation of \(T^\omega_{\mu+}\)-proofs to \(T^{\text{pre}}_\mu\)-proofs. As a corollary, it also gives a new proof of completeness of \(T^{\text{pre}}_\mu\) and of the finite model property of the modal \(\mu\)-calculus.
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 5529386
zbMATH Keywords: modal \(\mu\)-calculus
zbMATH Keywords: proof translation
zbMATH Keywords: infinitary proofs
zbMATH Keywords: finite model property
describes a project that uses: TTM
MaRDI profile type: Publication
OpenAlex ID: W2081909835
cites work: Modal logics and mu-calculi: An introduction
cites work: Sequent calculi for induction and infinite descent
cites work: Cut-free sequent systems for temporal logic
cites work: Syntactic Cut-elimination for Common Knowledge
cites work: A Proof System for the Linear Time μ-Calculus
cites work: The Complexity of Tree Automata and Logics of Programs
cites work: Propositional dynamic logic of regular programs
cites work: A Cut-Free and Invariant-Free Sequent Calculus for PLTL
cites work: Cut-free common knowledge
cites work: Canonical completeness of infinitary \(\mu \)
cites work: Results on the propositional \(\mu\)-calculus
cites work: A finite model theorem for the propositional \(\mu\)-calculus
cites work: Q3919674
cites work: Games for the \(\mu\)-calculus
cites work: Q4738237
cites work: Q4417874
cites work: Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
DOI: 10.1007/S11225-008-9133-6
Recommended article: On the expressivity of the modal mu-calculus
Recommended article: Modal logics and mu-calculi: An introduction
Recommended article: On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
Recommended article: On modal \(\mu \)-calculus and Gödel-Löb logic
Recommended article: Q4525272
Recommended article: Q4994684
Recommended article: Q3002404
Recommended article: Q4411834
Recommended article: Results on the propositional \(\mu\)-calculus
Recommended article: Q4681890
description: scientific article; zbMATH DE number 5529386