Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-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) | 335-353 |
| Publisher | Cham: Springer |
| Organisations |
|
| Abstract | We show how to construct uniform interpolants in the context of the modal mu-calculus. D’Agostino and Hollenberg (2000) were the first to prove that this logic has the uniform interpolation property, employing a combination of semantic and syntactic methods. This article outlines a purely proof-theoretic approach to the problem based on insights from the cyclic proof theory of mu-calculus. We argue the approach has the potential to lend itself to other temporal and fixed point logics. |
| Document type | Conference contribution |
| Language | English |
| Published at |
https://doi.org/10.1007/978-3-030-86059-2_20
(Final published version)
|
| Permalink to this page | |
