On the structure of inductive reasoning: circular and tree-shaped proofs in the mu-calculus
Christoph Sprenger, Mads Dam · 2003
We investigate a Gentzen-style proof system for the first-order $\mu $-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system use ...