The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Published: |
Kluwer
2000
|
| Online Access: | https://eprints.nottingham.ac.uk/343/ |
| _version_ | 1848790395833548800 |
|---|---|
| author | Dennis, Louise Abigail Bundy, Alan Green, Ian |
| author_facet | Dennis, Louise Abigail Bundy, Alan Green, Ian |
| author_sort | Dennis, Louise Abigail |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:11:56Z |
| format | Article |
| id | nottingham-343 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:56Z |
| publishDate | 2000 |
| publisher | Kluwer |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3432020-05-04T20:32:56Z https://eprints.nottingham.ac.uk/343/ The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction Dennis, Louise Abigail Bundy, Alan Green, Ian 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. Kluwer 2000 Article PeerReviewed Dennis, Louise Abigail, Bundy, Alan and Green, Ian (2000) The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction. Annals of Mathematics and Artificial Intelligence, 29 (1-4). pp. 99-138. |
| spellingShingle | Dennis, Louise Abigail Bundy, Alan Green, Ian The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction |
| title | The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction |
| title_full | The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction |
| title_fullStr | The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction |
| title_full_unstemmed | The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction |
| title_short | The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction |
| title_sort | productive use of failure to generate witnesses from divergent proof attempts for coinduction |
| url | https://eprints.nottingham.ac.uk/343/ |