Analogy as a Control Strategy in Theorem Proving

Authors:

• Erica Melis, Universitat des Saarlandes, FB Informatik, melis@cs.uni-sb.de
• Jon Whittle, Dept of AI, Edinburgh University, jonathw@dai.ed.ac.uk

Abstract:

We investigate analogy-driven proof plan construction as a control strategy in proof planning. The decisions taken in planning a source theorem are replayed for planning a similar target theorem. Our analogy procedure, ABALONE, implemented on top of the proof planner clam, is capable of a controlled replay of the source planning process. ABALONE provides additional control at key points of the target planning process by suggesting induction schemes, speculating lemmas, and patching failed plans.

Keywords:

Analogy, Theorem Proving, Proof Planning