TY - JOUR
T1 - Productive Use of Failure in Inductive Proof
AU - Ireland, A.
AU - Bundy, Alan
PY - 1996/3
Y1 - 1996/3
N2 - Proof by mathematical induction gives rise to various kinds of eureka steps, e.g., missing lemmata and generalization. Most inductive theorem provers rely upon user intervention in supplying the required eureka steps. In contrast, we present a novel theorem-proving architecture for supporting the automatic discovery of eureka steps. We build upon rippling, a search control heuristic designed for inductive reasoning. We show how the failure if rippling can be used in bridging gaps in the search for inductive proofs.
AB - Proof by mathematical induction gives rise to various kinds of eureka steps, e.g., missing lemmata and generalization. Most inductive theorem provers rely upon user intervention in supplying the required eureka steps. In contrast, we present a novel theorem-proving architecture for supporting the automatic discovery of eureka steps. We build upon rippling, a search control heuristic designed for inductive reasoning. We show how the failure if rippling can be used in bridging gaps in the search for inductive proofs.
U2 - 10.1007/BF00244460
DO - 10.1007/BF00244460
M3 - Article
VL - 16
JO - Journal of Automated Reasoning
T2 - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
SN - 0168-7433
IS - 1-2
ER -