PAMM
Volume 16, Issue 1 pp. 893-894
Section 25
Free Access

Circular proofs for the modal mu-calculus

Bahareh Afshari, 

Corresponding Author

Bahareh Afshari

Institut für Diskrete Mathematik und Geometrie, TU Wien, Wiedner Hauptstraße 8-10, Wien 1040, Austria

phone +43 158 801 104 281 fax +43 158 801 104 99Search for more papers by this author
Graham E. Leigh, 

Graham E. Leigh

Institut für Diskrete Mathematik und Geometrie, TU Wien, Wiedner Hauptstraße 8-10, Wien 1040, Austria

Search for more papers by this author
First published: 25 October 2016
https://doi.org/10.1002/pamm.201610435
Citations: 2

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)

The full text of this article hosted at iucr.org is unavailable due to technical difficulties.