Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #766 | |
|---|---|
| Title: | Analogy in Clam |
| Authors: | Melis,E |
| Date: | Aug 1995 |
| Presented: | Presented at IJCAI, August, 1995 |
| Keywords: | |
| Abstract: | CLAM is a proof planner, developed by the Dream group in Edinburgh, that mainly operates for inductive proofs. This paper addresses the question how an analogy model that I developed independently of CLAM can be applied to CLAM and it presents analogy-driven proof plan construction as a control strategy of CLAM. This strategy is realized as a derivational analogy that includes the reformulation of proof plans. The analogical replay checks whether the reformulated justifications of the source plan methods hold in the target as a permission to transfer the method to the target plan. Since CLAM has very efficient heuristic search strategies, the main purpose of the analogy is to suggest lemmas, to replan not commonly loaded methods to suggest induction variables and induction terms, and to overwrite control rather than to construct a target proof plan that could be built by CLAM itself more efficiently. |
| 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}