Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics Report Series >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1842/3396

This item has been viewed 2 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
0004.pdf358.13 kBAdobe PDFView/Open
Title: Making a Productive Use of Failure to Generate Witnesses for Coinduction from Divergent Proof Attempts
Authors: Dennis, Louise
Bundy, Alan
Green, Ian
Issue Date: 1999
Series/Report no.: Informatics Report Series
EDI-INF-RR-0004
Abstract: Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded 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 which 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.
Keywords: Informatics
URI: http://hdl.handle.net/1842/3396
Appears in Collections:Informatics Report Series

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy