Using a Generalisation Critic to find Bisimulations for Coinductive Proofs
Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that bisimilarity is a congruence in various domains it can be used to prove the congruence of two processes....
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
Springer
1999
|
| Online Access: | https://eprints.nottingham.ac.uk/344/ |
| _version_ | 1848790396093595648 |
|---|---|
| author | Dennis, Louise Abigail Bundy, Alan Green, Ian |
| author2 | McCune, William |
| author_facet | McCune, William Dennis, Louise Abigail Bundy, Alan Green, Ian |
| author_sort | Dennis, Louise Abigail |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that bisimilarity is a congruence in various domains it can be used to prove the congruence of two processes.
A coinductive proof requires a relation to be chosen which can be proved to be a bisimulation. We use proof planning to develop a heuristic method which automatically constucts a candidate relation. If this relation doesn't allow the proof to go through a proof critic analyses the reasons why it failed and modifies the relation accordingly.
Several proof tools have been developed to aid coinductive proofs but all require user interaction. Crucially they require the user to supply an appropriate relation which the system can then prove to be a bisimulation. |
| first_indexed | 2025-11-14T18:11:57Z |
| format | Conference or Workshop Item |
| id | nottingham-344 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:57Z |
| publishDate | 1999 |
| publisher | Springer |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3442020-05-04T20:33:06Z https://eprints.nottingham.ac.uk/344/ Using a Generalisation Critic to find Bisimulations for Coinductive Proofs Dennis, Louise Abigail Bundy, Alan Green, Ian Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that bisimilarity is a congruence in various domains it can be used to prove the congruence of two processes. A coinductive proof requires a relation to be chosen which can be proved to be a bisimulation. We use proof planning to develop a heuristic method which automatically constucts a candidate relation. If this relation doesn't allow the proof to go through a proof critic analyses the reasons why it failed and modifies the relation accordingly. Several proof tools have been developed to aid coinductive proofs but all require user interaction. Crucially they require the user to supply an appropriate relation which the system can then prove to be a bisimulation. Springer McCune, William 1999 Conference or Workshop Item PeerReviewed Dennis, Louise Abigail, Bundy, Alan and Green, Ian (1999) Using a Generalisation Critic to find Bisimulations for Coinductive Proofs. In: 14th International Conference on Automated Deduction (CADE-14), 1999, Townsville, Australia. |
| spellingShingle | Dennis, Louise Abigail Bundy, Alan Green, Ian Using a Generalisation Critic to find Bisimulations for Coinductive Proofs |
| title | Using a Generalisation Critic to find Bisimulations for Coinductive Proofs |
| title_full | Using a Generalisation Critic to find Bisimulations for Coinductive Proofs |
| title_fullStr | Using a Generalisation Critic to find Bisimulations for Coinductive Proofs |
| title_full_unstemmed | Using a Generalisation Critic to find Bisimulations for Coinductive Proofs |
| title_short | Using a Generalisation Critic to find Bisimulations for Coinductive Proofs |
| title_sort | using a generalisation critic to find bisimulations for coinductive proofs |
| url | https://eprints.nottingham.ac.uk/344/ |