A Focus System for the Alternation-Free μ-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) 371-388
Publisher Cham: Springer
Organisations
  • Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
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
Permalink to this page
Back