Cyclic proof systems for the alternation-free modal fixpoint logic
Johannes Marti
- 11:00 21st March 2023 ( week 10, Hilary Term 2023 )Room 051
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.