TY - BOOK
T1 - Using failure to guide inductive proof
AU - Ireland,Andrew
AU - Bundy,Alan
PY - 1992
Y1 - 1992
N2 - 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.
AB - 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.
M3 - Book
BT - Using failure to guide inductive proof
PB - University of Edinburgh, Department of Artificial Intelligence
ER -