Focus-style proof systems and interpolation for the alternation-free $μ$-calculus
Johannes Marti, Yde Venema · arXiv (Cornell University) · 2021
In this paper we introduce a cut-free sequent calculus for the alternation-free fragment of the modal $μ$-calculus. This system allows for cyclic 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 and apply it to prove that the alternation-free fragment has the Craig interpolation property.