A Model of Analogy-Driven Proof-Plan Construction

Abstract

This paper addresses a model of analogy-driven theorem proving that is more general and cognitively more adequate than previous approaches. The model works at the level of proof-plans. More precisely, we consider analogy as a control strategy in proof planning that employs a source proof- plan to guide the construction of a proof-plan for the target problem. Our approach includes a reformulation of the source proof-plan. This is in accordance with the well known fact that constructing an analogy in maths often amounts to first finding the appropriate representation which brings out the similarity of two problems, i.e., finding the right concepts and the right level of abstraction . Several well known theorems were processed by our analogy-driven proof- plan construction that could not be proven analogically by previous approaches.