DocumentCode
2070884
Title
A methodology for equational reasoning
Author
Cleve, Jürgen ; Hutter, Dieter
Author_Institution
German Res. Center for Artificial Intelligence, Saarbrucken, Germany
Volume
3
fYear
1994
fDate
4-7 Jan. 1994
Firstpage
569
Lastpage
578
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/HICSS.1994.323323
Filename
323323
Link To Document