Cyclic proofs for the first-order μ-calculus
| Authors |
|
|---|---|
| Publication date | 02-2024 |
| Journal | Logic Journal of the IGPL |
| Volume | Issue number | 32 | 1 |
| Pages (from-to) | 1–34 |
| Number of pages | 34 |
| Organisations |
|
| Abstract | We introduce a path-based cyclic proof system for first-order μ-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 μ-calculus. |
| Document type | Article |
| Language | English |
| Published at | https://doi.org/10.1093/jigpal/jzac053 |
| Downloads |
jzac053
(Final published version)
|
| Permalink to this page | |
