CIRC : A Circular Coinductive Prover

Abstract. CIRC is an automated circular coinductive prover implemented as an extension of Maude. The circular coinductive technique that forms the core of CIRC is discussed, together with a high-level implementation using metalevel capabilities of rewriting logic. To reflect the strength of CIRC in automatically proving behavioral properties, an example defining and proving properties about infinite streams of infinite binary trees is shown. CIRC also provides limited support for automated inductive proving, which can be used in combination with coinduction.

• Type: Conference
• Year: 2007
• Where: CALCO
• Authors: Dorel Lucanu, Grigore Rosu
• Keywords: CALCO 2007, CIRC, Circular Coinductive Prover, Circular Coinductive Technique, Mathematics