Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #845 | |
|---|---|
| Title: | Equalizing Terms by Difference Reduction Techniques |
| Authors: | Hutter,D |
| Date: | Feb 1997 |
| Presented: | In the Proceedings of the 10th Annual Florida AI Research Symposium, FLAIRS'97 |
| Keywords: | |
| Abstract: | In the field of inductive theorem proving syntactical differences between the induction hypothesis and induction conclusion are used in order to guide the proof [BvHS91, Hut90, Hut]. This method of guiding induction proofs is called rippling / coloring terms and there is considerable evidence of its success on practical examples. For equality reasoning we use these annotated terms to represent syntactical differences of formulas. Based on these annotations and on hierarchies of function symbols we define different abstractions of formulas which are used for a hierarchical planning of proofs. Also rippling techniques are used to refine single planning steps, e.g. the application of a bridge lemma, on a next planning level. |
| 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}