|
Abstract : |
Abstract. In this paper we present an approach to prove the equality between terms in a goaldirected way developed in the field of inductive theorem proving. The two terms to be equated are syntactically split into expressions which are common to both and those which occur only in one term. According to the computed differences we apply appropriate equations to the terms in order to reduce the differences in a goal-directed way. Although this approach was developed for purposes of inductive theorem proving- we use this technique to manipulate the conclusion of an induction step to enable the use of the hypothesis- it is a powerful method for the control of equational reasoning in general. 1., |
