Research Repository

See what's under the surface

Using a Generalisation Critic to find Bisimulations for Coinductive Proofs

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

Authors

Louise Abigail Dennis

Alan Bundy

Ian Green



Contributors

William McCune
Editor

Abstract

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.

Publication Date Jan 1, 1999
Peer Reviewed Peer Reviewed
Institution Citation Dennis, L. A., Bundy, A., & Green, I. (1999). Using a Generalisation Critic to find Bisimulations for Coinductive Proofs. In W. McCune (Ed.),
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
Additional Information Lecture Notes in Artificial Intelligence 1294

Files

coinduction.ps (165 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