The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #834

Title:Using a Generalisation Critic to Find Bisimulations for Coinductive Proofs
Authors:Dennis,L; Bundy,A; Green,I
Date:Dec 1996
Presented:Submitted to CADE 14
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 observational equivalenc is a congruence in various domains it can be used to proof the congruence of two processes. 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. A method is proposed which uses the idea of proof plans to make a heuristic guess at a suitable relation. If the proof fails for that relation the reasons for failure are analysed using a proof critic and a new relation is proposed to allow the proof to go through.

[Search These Pages] [DAI Home Page] [Comment]