On global induction mechanisms in a μ-calculus with explicit approximations
INRIA Sophia Antipolis, 2004, route des Lucioles, BP 93, 06902 Sophia
Antipolis, France; email@example.com.
2 Dept. of Microelectronics and Information Technology, Royal Institute of Technology, KTH, Forum 105, 164 40 Kista, Sweden; firstname.lastname@example.org.
Accepted: 31 October 2003
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.
Mathematics Subject Classification: 68Q60 / 03F07 / 03B35
Key words: Inductive reasoning / circular proofs / well-foundedness / global consistency condition / μ-calculus / approximants.
© EDP Sciences, 2003