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

Research Paper #613

Title:Using Failure to Guide Inductive Proof
Authors:Ireland,A; Bundy,A
Date: 1992
Presented:Submitted to IJCAI'93
Abstract:Lemma discovery and generalization are two of the major hurdles in automating inductive proof. This paper addresses aspects of these related problems. We build upon rippling, a heuristic which plays a pivotal role in guiding inductive proof. Rippling provides a high-level explanation of how to control the search for a proof. We demonstrate how this high-level explanation can be exploited productively when a proof attempt fails. In particular we show how failure can be used to focus the search for lemmas and generalizations.

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