Using failure to guide inductive proof

Andrew Ireland, Alan Bundy

Research output: Book/ReportBook

Abstract / Description of output

Lemma discovery and generalization are two of the ma jor 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.
Original languageEnglish
PublisherUniversity of Edinburgh, Department of Artificial Intelligence
Publication statusPublished - 1992


Dive into the research topics of 'Using failure to guide inductive proof'. Together they form a unique fingerprint.

Cite this