Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #9594 | |
|---|---|
| Title: | Analogy in Clam |
| Authors: | Whittle,JN |
| Date: | 1995 |
| Presented: | |
| Keywords: | |
| Abstract: | This thesis investigates the possibility of incorporating two types of analogy - internal and external - into the inductive proof planner CLAM. CLAM's induction revision critic revises an incorrectly chosen induction scheme. Internal analogy is used to suggest induction schemes thus reducing the need to apply this critic repeatedly. The time taken to plan certain theorems was reduced as a result. External analogy is used to derive the step-case of the proof plan for a target theorem given the plan of an analogous source theorem. The paradigm used is derivational analogy, whereby problem-solving decisions used in the source are replayed in the target. Reformulations of the source plan are necessary in some cases. The resulting system, ABALONE, proved capable of suggesting target induction schemes and target lemmata that could be used in the target plan. It can also be used to replay not commonly loaded methods and to generalise variables apart in the target conjecture. Unfortunately, it proved difficult to find examples that could be planned by analogy but that are presently beyond the scope of CLAM. |
| 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}