A Methodology for Equational Reasoning

1 This paper presents a methodology to guide equational reasoning in a goal directed way. Suggested by rippling methods developed in the eld 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 di erence uni cation and rippling to enable its use.

• Type: Conference
• Year: 1994
• Where: HICSS
• Authors: Jürgen Cleve, Dieter Hutter
• Keywords: Biometrics, Bridge Lemma, Goal Directed Way, HICSS 1994, Theorem Proving