Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #9910 | |
|---|---|
| Title: | Generalisation as a critic to the induction strategy |
| Authors: | MacLean,EA |
| Date: | 1999 |
| Presented: | |
| Keywords: | |
| 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. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}