CoCLAM
swMATH ID:  28719 
Software Authors:  Dennis, L. A.; Bundy, A.; Green, I. 
Description:  Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts. Coinduction is a proof rule. It is the dual of induction. It allows reasoning about nonwellfounded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called a bisimulation). We present an automation of coinductive theorem proving. This automation is based on the idea of proof planning. Proof planning constructs the higher level steps in a proof, using knowledge of the general structure of a family of proofs and exploiting this knowledge to control the proof search. Part of proof planning involves the use of failure information to modify the plan by the use of a proof critic exploits the information gained from the failed proof attempt. Our approach to the problem was to develop a strategy that makes an initial simple guess at a bisimulation and then uses generalisation techniques, motivated by a critic, to refine this guess, so that a larger class of coinductive problems can be automatically verified. The implementation of this strategy has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell. We have developed a proof plan for coinduction and a critic associated with this proof plan. These have been implemented in CoCLAM, an extended version of CLAM, with encouraging results. The planner has been successfully tested on a number of theorems. 
Homepage:  https://link.springer.com/article/10.1023%2FA%3A1018940332714 
Keywords:  proof planning; CoCLAM 
Related Software:  Oyster; OMEGA; CLAM; Concurrency Workbench; HOL 
Referenced in:  2 Publications 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts. Zbl 1001.68128 Dennis, L. A.; Bundy, A.; Green, I. 
2000

all
top 5
Referenced by 8 Authors
1  Bundy, Alan 
1  Cabrera, Inma P. 
1  Cordero, Pablo 
1  Dennis, Louise Abigail 
1  Green, Ian 
1  Gutiérrez, Gloria 
1  Martínez del Castillo, Javier 
1  OjedaAciego, Manuel 
Referenced in 2 Serials
1  Applied Mathematics and Computation 
1  Annals of Mathematics and Artificial Intelligence 
Referenced in 3 Fields
1  Order, lattices, ordered algebraic structures (06XX) 
1  General algebraic systems (08XX) 
1  Computer science (68XX) 