Cyclic proofs for the first-order µ-calculus

Logic Journal of the IGPL (forthcoming)
  Copy   BIBTEX


We introduce a path-based cyclic proof system for first-order $\mu $-calculus, the extension of first-order logic by second-order quantifiers for least and greatest fixed points of definable monotone functions. We prove soundness of the system and demonstrate it to be as expressive as the known trace-based cyclic systems of Dam and Sprenger. Furthermore, we establish cut-free completeness of our system for the fragment corresponding to the modal $\mu $-calculus.



    Upload a copy of this work     Papers currently archived: 94,517

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

19 (#809,166)

6 months
12 (#312,853)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

References found in this work

No references found.

Add more references