TY - GEN
T1 - Using a generalisation critic to find bisimulations for coinductive proofs
AU - Dennis,Louise
AU - Bundy,Alan
AU - Green,Ian
PY - 1997
Y1 - 1997
N2 - 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 constructs a candidate relation. If this relation does not 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.
AB - 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 constructs a candidate relation. If this relation does not 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.
KW - coinduction
KW - proof planning
KW - proof critics
U2 - 10.1007/3-540-63104-6_29
DO - 10.1007/3-540-63104-6_29
M3 - Conference contribution
SN - 978-3-540-63104-0
T3 - Lecture Notes in Computer Science
SP - 276
EP - 290
BT - Automated Deductionâ€”CADE-14
PB - Springer-Verlag GmbH
ER -