Circular proofs for the modal mu‐calculus
Bahareh Afshari, Graham E. Leigh · PAMM · 2016
Abstract Inspired by Stirling's tableau proofs [4] we introduce a finite, cut‐free sound and complete sequent calculus for the modal mu‐calculus. Proofs in this system are finite trees in which leaves are either axioms or assumptions that are discharged by a specific rule of the calculus. The discharge rules provide a way to unfold assumptions motivating the name circular proofs. (© 2016 Wiley‐VCH Verlag GmbH & Co. KGaA, Weinheim)