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/ |