Skip to main content

Research Repository

See what's under the surface

Advanced Search

The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction

Dennis, Louise Abigail; Bundy, Alan; Green, Ian

Authors

Louise Abigail Dennis

Alan Bundy

Ian Green



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.

Journal Article Type Article
Publication Date Jan 1, 2000
Journal Annals of Mathematics and Artificial Intelligence
Print ISSN 1012-2443
Publisher Humana Press
Peer Reviewed Peer Reviewed
Volume 29
Issue 1-4
APA6 Citation Dennis, L. A., Bundy, A., & Green, I. (2000). The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction. Annals of Mathematics and Artificial Intelligence, 29(1-4),
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf

Files

amai.ps (651 Kb)
Other

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





Downloadable Citations

;