Cyclic proof systems for the alternation-free modal fixpoint logic

I present a cut-free sequent calculus that is sound and complete for the alternation-free fragment of the modal mu-calculus. The system allows for cyclic proofs, which arise naturally from unravelling fixpoint operators. A special focus mechanism is used to ensure that proofs only contain cycles that are logically sound.