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

MSc Thesis #93139

Title:Coloured Rippling
Date: 1993
Abstract:Inductive proofs can be used to prove properties of computer programs formally and to bring reliability into computer program design. Proof Planning aims at capturing the way human mathematicians construct inductive proofs and has proved highly successful in guiding the search for the automated construction of inductive proofs. However, until now the theorems which have data-structures with multiple recursive arguments have not been tried intensively. This dissertation describes the implementation of an extension to the Clam proof planning system which can prove such theorems. Putting "colours" on the proper subterm in the induction conclusion is the key idea behind this work. These "colours" guide the search in the construction of inductive proofs so that the different copies of induction hypotheses can be identified and used to prove the induction conclusion. The system can now prove then theorems which have binary tree structures and two limit theorems. Possible extensions of the current system are also suggested in this dissertation.

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