Show simple item record

Proceedings of the 10th International Conference on Automated Deduction

dc.contributor.authorBundy, Alan
dc.contributor.authorvan Harmelen, F.
dc.contributor.authorSmaill, A.
dc.contributor.authorIreland, A.
dc.date.accessioned2011-01-28T17:07:17Z
dc.date.available2011-01-28T17:07:17Z
dc.date.issued1990
dc.identifier.isbn3-540-52885-7en
dc.identifier.urihttp://www.springerlink.com/content/75021890103xh7h3/en
dc.identifier.urihttp://hdl.handle.net/1842/4701
dc.description.abstractIn 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.en
dc.language.isoenen
dc.publisherSpringer Verlagen
dc.titleExtensions to the Rippling-Out Tactic for Guiding Inductive Proofsen
dc.typeConference Paperen
dc.identifier.doi10.1007/3-540-52885-7_84en
rps.volumeLecture Notes in Artificial Intelligence No. 449en
rps.titleProceedings of the 10th International Conference on Automated Deductionen
dc.extent.noOfPages132-146en
dc.extent.pageNumbers132-146en
dc.date.updated2011-01-28T17:07:17Z
dc.date.openingDate1990-07-24
dc.date.closingDate1990-07-27


Files in this item

This item appears in the following Collection(s)

Show simple item record