Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #803 | |
|---|---|
| Title: | Internal Analogy in Theorem Proving |
| Authors: | Melis,E; Whittle,JN |
| Date: | Apr 1996 |
| Presented: | Published in the Proceedings of CADE-13, 1996 |
| Keywords: | |
| Abstract: | Internal analogy tries to reuse solutions of subproblems within the same problem solving process. In mathematical theorem proving several patterns are known where internal analogy suggests itself. Hence, we propose the use of internal analogy in automated theorem proving. This paper investigates the possibility of incorporating internal analogy into the inductive proof planner CLAM. It introduces internal analogy as a control strategy of CLAM that can reduce search. We concentrate on using internal analogy to avoid the repeated application of the induction revision critic. The implementation has been tested and it wasfound that internal analogy can reduce the time taken to construct proof plans for some theorems. |
| 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}