Edinburgh Research Archive >
Informatics, School of >
Informatics Publications >
Please use this identifier to cite or link to this item:
|Title: ||Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs|
|Authors: ||Bundy, Alan|
van Harmelen, F.
|Issue Date: ||1990|
|Journal Title: ||Proceedings of the 10th International Conference on Automated Deduction|
|Volume: ||Lecture Notes in Artificial Intelligence No. 449|
|Page Numbers: ||132-146|
|Publisher: ||Springer Verlag|
|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.|
|Appears in Collections:||Informatics Publications|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.