Title :
A methodology for equational reasoning
Author :
Cleve, Jürgen ; Hutter, Dieter
Author_Institution :
German Res. Center for Artificial Intelligence, Saarbrucken, Germany
Abstract :
Presents a methodology to guide equational reasoning in a goal-directed way. Suggested by rippling methods developed in the field of inductive theorem proving, we use attributes of terms and heuristics to determine bridge lemmas, i.e. lemmas which have to be used during the proof of the theorem. Once we have found such a bridge lemma, we use the techniques of difference unification and rippling to enable its use.<>
Keywords :
equations; model-based reasoning; theorem proving; bridge lemmas; difference unification; equational reasoning methodology; goal-directed guidance; heuristics; inductive theorem proving; rippling methods; term attributes;
Conference_Titel :
System Sciences, 1994. Proceedings of the Twenty-Seventh Hawaii International Conference on
Conference_Location :
Wailea, HI, USA
Print_ISBN :
0-8186-5090-7
DOI :
10.1109/HICSS.1994.323323
