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

Research Paper #841

Title:Analogy in Inductive Theorem Proving
Authors:Melis,E; Whittle,JN
Date:Dec 1996
Presented:Submitted to the 14th Conference on Automated Deduction
Abstract:This paper investigates analogy-driven proof plan construction in inductive theorem proving. We identify constraints of second-order mappings that enable a replay of the plan of a source theorem to produce a similar plan for the target theorejm. In some cases, differences between the source andtarget theorem mean that the target proof plan has to be reformulated. These reformulations are sugested by the mappings. The analogy procedure, implemented in ABALONE, is particularly useful for overriding the default control and suggesting lemmas. Employing analogy has extended the prolem solving horizon of the proof planner CLAM: with analogy, some theorems could be proved that neither CLAM nor NQTHM could prove automatically.

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