Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #841 | |
|---|---|
| Title: | Analogy in Inductive Theorem Proving |
| Authors: | Melis,E; Whittle,JN |
| Date: | Dec 1996 |
| Presented: | Submitted to the 14th Conference on Automated Deduction |
| Keywords: | |
| Abstract: | This paper investigates analogy-driven proof plan construction in inductive theorem proving. We identify constraints of second-order mappings that enable a replay of the plan of a source theorem to produce a similar plan for the target theorejm. In some cases, differences between the source andtarget theorem mean that the target proof plan has to be reformulated. These reformulations are sugested by the mappings. The analogy procedure, implemented in ABALONE, is particularly useful for overriding the default control and suggesting lemmas. Employing analogy has extended the prolem solving horizon of the proof planner CLAM: with analogy, some theorems could be proved that neither CLAM nor NQTHM could prove automatically. |
| Download: | POSTSCRIPT 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}