The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #845

Title:Equalizing Terms by Difference Reduction Techniques
Date:Feb 1997
Presented:In the Proceedings of the 10th Annual Florida AI Research Symposium, FLAIRS'97
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.

[Search These Pages] [DAI Home Page] [Comment]