Analogy in inductive theorem proving

In this paper, we investigate analogy-driven proof plan construction in inductive theorem proving. The intention is to produce a plan for a target theorem that is similar to a given source theorem. We identify second-order mappings from the source to the target that preserve induction-specific proof-relevant abstractions dictating whether the source plan can be replayed. We replay the planning decisions taken in the source if the reasons or justifications for these decisions still hold in the target. If the source and target plan differ significantly at some isolated point, additional reformulations are invoked to add, delete, or modify planning steps. These reformulations are not ad hoc but are triggered by peculiarities of the mappings and by failed justifications. Employing analogy on top of the proof planner CLAM has extended the problem-solving horizon of CLAM: With analogy, some theorems could be proved automatically that neither CLAM nor NQTHM could prove automatically.