Effective cut-elimination for a fragment of modal mu-calculus
The mu-calculus is an extension of temporal logic for transition systems with added fixpoint operators which appeared particularly useful for specification and verification of temporal properties. An infinitary system adequate for the whole mu-calculus was proved cut-free in a non-constructive way by \textit{G. Jäger}, \textit{M. Kretz} and \textit{T. Studer} in [J. Log. Algebr. Program. 76, No. 2, 270--292 (2008; Zbl 1156.68013)]. A constructive proof of cut elimination for the fragment of mu-calculus, called \(\mathrm{M}_1\), with non-iterated fixpoints and omega-rule was offered by \textit{W. Buchholz} in [Arch. Math. Logic 40, No. 4, 255--272 (2001; Zbl 1007.03051)], but only for positive formulas. In this paper, G. Mints provides another constructive proof of cut elimination for \(\mathrm{M}_1\) which improves Buchholz's result in two ways. First, it is not restricted to proofs of positive formulas. Second, the omega-rule is only an intermediate tool for obtaining a cut-free calculus. In order to remove cut from \(\mathrm{M}_1\), the system \(\mathrm{M}^\prime\) is introduced, which is cut-free but uses instead of the (finitary) rule (ind) of \(\mathrm{M}_1\) some infinitary rule. Next, the auxiliary system \(\mathrm{M}^\Omega \) is introduced which adds to \(\mathrm{M}^\prime\) two omega-rules and a form of cut. It is shown that every derivation in \(\mathrm{M}_1\) is transformed into a derivation in \(\mathrm{M}^\Omega \), and every derivation in \(\mathrm{M}^\Omega \) is transformed into a derivation in \(\mathrm{M}^\prime\). Although this result by itself does not imply cut admissibility for \(\mathrm{M}_1\), there are simple sufficient conditions satisfied by Mints's proof which recovers provability in the finitary system from provability in the infinitary one. As a result, cut admissibility for \(\mathrm{M}_1\) follows. The text is rather dense and technical, hence the reader not acquainted with the mu-calculus should first consult some introductory paper, e.g., \textit{J. Bradfield} and \textit{C. Stirling}'s survey in [``Modal mu-calculus, in: Handbook of modal logic. Amsterdam: Elsevier. 721--756 (2007; Zbl 1114.03001)].
- A Buchholz rule for modal fixed point logics
- A focus system for the alternation-free \(\mu \)-calculus
- On the proof theory of the modal mu-calculus
- scientific article; zbMATH DE number 1956572
- On the universal and existential fragments of the \(\mu\)-calculus
- On model checking for the -calculus and its fragments
- scientific article; zbMATH DE number 7324390
- scientific article; zbMATH DE number 7297836
- Logic for Programming, Artificial Intelligence, and Reasoning
- scientific article; zbMATH DE number 1927555
- A Buchholz rule for modal fixed point logics
- A finite model theorem for the propositional \(\mu\)-calculus
- An extension of the omega-rule
- Canonical completeness of infinitary \(\mu \)
- Explaining the Gentzen-Takeuti reduction steps: A second-order system
- Proof theory. 2nd ed
- Proof theory. The first step into impredicativity
- Syntactic cut-elimination for common knowledge
- A Buchholz rule for modal fixed point logics
- An infinitary treatment of full \(\mu\)-calculus
- An extension of the omega-rule
- scientific article; zbMATH DE number 1405663 (Why is no real title available?)
- scientific article; zbMATH DE number 7297836 (Why is no real title available?)
- On the cut-elimination of the modal -calculus: linear logic to the rescue
- Syntactic cut-elimination for a fragment of the modal mu-calculus
This page was built for publication: Effective cut-elimination for a fragment of modal mu-calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q454366)
