On global induction mechanisms in a μ-calculus with explicit approximations

¹ INRIA Sophia Antipolis, 2004, route des Lucioles, BP 93, 06902 Sophia Antipolis, France; sprenger@sophia.inria.fr.
² Dept. of Microelectronics and Information Technology, Royal Institute of Technology, KTH, Forum 105, 164 40 Kista, Sweden; mfd@imit.kth.se.

Received: 8 November 2002
Accepted: 31 October 2003

Abstract

We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic condition. We give an automata-theoretic reformulation of this condition which is more suitable for practical proofs. For a detailed comparison with previous work we consider two simpler syntactic conditions and show that they are more restrictive than our new condition.