The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #840

Title:Analogy as a Control Strategy in Theorem Proving
Authors:Melis,E; Whittle,JN
Date:Dec 1996
Presented:Accepted for the 10th International FLAIRS Conference
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. In addition to the pure replay of source planning decisions, ABALONE can provide control, e.g. by overriding the default control and suggesting both induction schemes and lemnas needed in the planning process.

[Search These Pages] [DAI Home Page] [Comment]