Edinburgh Research Explorer

Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions

Open

Original languageEnglish
Title of host publication10th International Conference on Automated Deduction
Subtitle of host publicationKaiserslautern, FRG, July 24–27, 1990 Proceedings
PublisherSpringer-Verlag GmbH
Pages132-146
VolumeLecture Notes in Artificial Intelligence No. 449
ISBN (Print)3-540-52885-7
DOIs
StatePublished - 1990

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume449
ISSN (Print)0302-9743

Abstract

In earlier papers we described a technique for automatically constructing inductive proofs, using a heuristic search control tactic called rippling-out. Further testing on harder examples has shown that the rippling-out tactic significantly reduces the search for a proof of a wide variety of theorems, with relatively few cases in which all proofs were pruned. However, it also proved necessary to generalise and extend rippling-out in various ways. Each of the various extensions are described with examples to illustrate why they are needed, but it is shown that the spirit of the original rippling-out tactic has been retained. The research reported in this paper was supported by SERC grant GR/E/44598, and an SERC Senior Fellowship to the first author. We wish to thank our colleagues in the Edinburgh Mathematical Reasoning Group and three anonymous referees for feedback on this paper.

Download statistics

No data available

ID: 403792