CIRC
Circ is an automated behavioral prover based on the circularity principle. The circularity principle generalizes both circular coinduction and structural induction 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. 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.
Keywords for this software
References in zbMATH (referenced in 40 articles , 2 standard articles )
Showing results 1 to 20 of 40.
Sorted by year (- Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
- Hansen, Helle Hvid; Kupke, Clemens; Rutten, Jan: Stream differential equations: specification formats and solution methods (2017)
- Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
- Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
- Babenyshev, Sergey; Martins, Manuel A.: Behavioral equivalence of hidden (k)-logics: an abstract algebraic approach (2016)
- Rot, Jurriaan; Bonsangue, Marcello; Rutten, Jan: Proving language inclusion and equivalence by coinduction (2016)
- Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Witnessing (co)datatypes (2015)
- Kozen, Dexter; Silva, Alexandra: Practical coinduction (2015)
- Lucanu, Dorel; Rusu, Vlad: Program equivalence by circular reasoning (2015)
- Pattinson, Dirk; Schröder, Lutz: Sound and complete equational reasoning over comodels (2015)
- Diaconescu, Răzvan: CafeOBJ traces (2014)
- Diaconescu, Răzvan; Ţuţu, Ionuţ: Foundations for structuring behavioural specifications (2014)
- Endrullis, Jörg; Hendriks, Dimitri; Bakhshi, Rena; Roşu, Grigore: On the complexity of stream equality (2014)
- Găină, Daniel; Lucanu, Dorel; Ogata, Kazuhiro; Futatsugi, Kokichi: On automation of OTS/CafeOBJ method (2014)
- Ogata, Kazuhiro; Futatsugi, Kokichi: Theorem proving based on proof scores for rewrite theory specifications of OTSs (2014)
- Roşu, Grigore; Lucanu, Dorel: Behavioral rewrite systems and behavioral productivity (2014)
- Găină, Daniel; Zhang, Min; Chiba, Yuki; Arimoto, Yasuhito: Constructor-based inductive theorem prover (2013)
- Martins, M. A.; Madeira, A.; Barbosa, L. S.: A coalgebraic perspective on logical interpretations (2013)
- Rot, Jurriaan; Bonsangue, Marcello; Rutten, Jan: Coinductive proof techniques for language equivalence (2013)
- Winter, Joost: Qstream: a suite of streams (2013) ioport