Edinburgh Research Explorer

Productive Use of Failure in Inductive Proof

Research output: Contribution to journalArticlepeer-review

Related Edinburgh Organisations

Open Access permissions



Original languageEnglish
JournalJournal of Automated Reasoning
Issue number1-2
Publication statusPublished - Mar 1996


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.

Download statistics

No data available

ID: 400455