Lyndon interpolation for modal μ-calculus

Open Access
Authors
Publication date 2022
Host editors
  • A. Özgün
  • Y. Zinova
Book title Language, Logic, and Computation
Book subtitle 13th International Tbilisi Symposium, TbiLLC 2019, Batumi, Georgia, September 16-20, 2019 : revised selected papers
ISBN
  • 9783030984786
  • 9783030984809
ISBN (electronic)
  • 9783030984793
Series Lecture Notes in Computer Science
Event 13th International Tbilisi Symposium on Language, Logic and Computation, TbiLLC 2019
Pages (from-to) 197–213
Publisher Cham: Springer
Organisations
  • Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
Abstract It is known that the modal μ-calculus has the Craig interpolation property, indeed uniform interpolation. We prove Lyndon interpolation for the calculus, a strengthening of Craig interpolation which is not implied by uniform interpolation. The proof utilises ‘cyclic’ sequent calculus and provides an algorithmic construction of interpolants from valid implications. This direct approach enables us to derive a correspondence between the shape of interpolants and existence of sequent calculus proofs.
Document type Conference contribution
Language English
Published at https://doi.org/10.1007/978-3-030-98479-3_10
Downloads
Afshari (Submitted manuscript)
Permalink to this page
Back