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

MSc Thesis #9910

Title:Generalisation as a critic to the induction strategy
Date: 1999
Abstract:Generalisation in mathematics is a technique that cannot only strengthen the significance of the result, but also help to prove theorems. In the context of inductive proofs the opportunity for generalisation often arises, and it is important to discover whether generalisation is necessary, in order to render a proof successful. The existence of the rippling- a heuristic guidance within proof-planning- helps to analyse whether generalisation should be applied. A human can often realise whether generalisation is required at the point where induction is attempted. The aim of this project is to determine whether this ability can be reproduced within a proof-planner. One of the techniques that is very useful in implementation, is the critics mechanism which analyses the failure of a proof and suggests patches to overcome the failure. We investigatethe possibility of determining whether generalisation can be successfully implemented by attaching critics to the induction strategy.We develop a system by which this claim can be tested, which includes three different types of generalisation. We also implement a simple version of a critic which analyses the failure of the proof at the point where no rewriting applies.

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