Productive use of failure in inductive proof

Andrew Ireland, Alan Bundy

Research output: Contribution to journalArticle

91 Citations (Scopus)

Abstract

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. © 1996 Kluwer Academic Publishers.

Original languageEnglish
Pages (from-to)79-111
Number of pages33
JournalJournal of Automated Reasoning
Volume16
Issue number1-2
Publication statusPublished - 1996

Keywords

  • Automated theorem proving
  • Mathematical induction
  • Proof patching

Fingerprint Dive into the research topics of 'Productive use of failure in inductive proof'. Together they form a unique fingerprint.

Cite this