Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus

Authors
Publication date 2021
Host editors
  • A. Das
  • S. Negri
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
  • 9783030860585
ISBN (electronic)
  • 9783030860592
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
  • Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
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
Permalink to this page
Back