Circ is an automated circular coinductive prover that is implemented as an
extension of Maude.
CIRC implements the circularity principle, which generalizes
circular coinductive deduction and can
be expressed in plain English as follows. Assume that each equation
of interest (to be proved) e admits a frozen form
fr(e) and a set of derived equations, its
derivatives, Der(e). The circularity principle
requires that the following rule be valid: if from the hypotheses
H together with fr(e) we can deduce
Der(e), then e is a consequence of H.
When fr(e) freezes the equation at the top,
the circularity principle becomes circular
coinduction. Interestingly, when the equation is frozen at the
bottom on a variable, then it becomes a structural induction (on that
variable) derivation rule. This way, CIRC supports both coinduction
and induction as projections of a more general principle.
Download CIRC 1.4: circ.maude- CIRC entire archive: circ.zip.
The archive includes documentation, a set of examples, and the tool circ.maude.
- Installing
- If you already have Maude installed, then go to the next step. Otherwise,
- if you work on a Linux platform, then go to
Maude download page
and follow the steps written there for downloading and installing Maude;
- if you work on a Windows platform, then go to
and download Maude for Windows;
- if you have Eclipse, then you also may download Maude
Development Tools from ;
this include a set of plug-ins embedding the Maude system into the Eclipse environment.
- Download CIRC tool circ.maude or the archive
circ.zip. The archive includes documentation
(this document), a set of examples, and the tool circ.maude.
- Copy the file circ.maude in the folder including Maude
tools (e.g., Full-Maude.maude, model-checker.maude and so on).
- Loading
- Start Maude in Full-Maude mode. If Full-Maude is not loaded
automatically, then introduce the command in full-maude.
- Load the prover introducing the command in circ.
- You may introduce now any CIRC or Full-Maude command.
- Running the Examples
- The system is accompanied by a set of examples exhibiting the power of
the prover. The usual scenario for running an example is:
- set the prover in the initial state introducing the command
Maude> loop init. In many cases this is an optional step.
- introduce Maude specifications using Maude command
in file-name. The files include specifications
and commands. The complete list of CIRC commands is included in
the user manual.
- CIRC Prover (includes a short tutorial and the user manual) [ps] [pdf]