Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #92138 | |
|---|---|
| Title: | Tailoring New Lemmas from Existing Theorems |
| Authors: | Pagonis,E |
| Date: | 1992 |
| Presented: | |
| Keywords: | |
| Abstract: | Recent work in Mathematical Reasoning Group at Edinburgh has centred around the notion of proof plans [Bundy et al 88] to guide the search for a proof in automatic theorem proving by mathematical induction. The central idea of the technique of inductive proof plans is a tactic called rippling-out, which manipulates the induction conclusion in order for the induction hypothesis to be used in its proof. So far this tactic has been surprisingly successful at reducing the search for a proof of a large number of inductive theorems. The problem, however, is that sometimes this tactic fails due to lack of the appropriate rewrite rule. In some cases, the required rewrite rule is a communicative/associative variation of well known theorems. The task of this project is to enable the current planning system to create the required rewrite rule dynamically, and make it available for the current proof. for this purpose, we developed a new method called ass-com. In addition, the second part of this project deals with situations where a specific term called the minimum "blockage term", causes rippling to be blocked. In order to handle these situations, we built the complement-ripple method, and as an extension to this method the gen-complement-ripple method. The three new methods mentioned above have been successful at unblocking rippling in a number of theorems. |
| 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}