A Focus System for the Alternation-Free μ-Calculus
| Authors | |
|---|---|
| Publication date | 2021 |
| Host editors |
|
| Book title | Automated Reasoning with Analytic Tableaux and Related Methods |
| Book subtitle | 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021 : proceedings |
| ISBN |
|
| ISBN (electronic) |
|
| Series | Lecture Notes in Computer Science |
| Event | 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods |
| Pages (from-to) | 371-388 |
| Publisher | Cham: Springer |
| Organisations |
|
| Abstract | We introduce a cut-free sequent calculus for the alternation-free fragment of the modal μ-calculus. This system allows both for infinite and for finite, circular proofs and uses a simple focus mechanism to control the unravelling of fixpoints along infinite branches. We show that the proof system is sound and complete for the set of guarded valid formulas of the alternation-free μ-calculus. |
| Document type | Conference contribution |
| Language | English |
| Published at |
https://doi.org/10.1007/978-3-030-86059-2_22
(Final published version)
|
| Permalink to this page | |