{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:46:01Z","timestamp":1768002361892,"version":"3.49.0"},"reference-count":19,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1993,8,1]],"date-time":"1993-08-01T00:00:00Z","timestamp":744163200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1993,8]]},"DOI":"10.1016\/0004-3702(93)90079-q","type":"journal-article","created":{"date-parts":[[2003,3,14]],"date-time":"2003-03-14T13:02:52Z","timestamp":1047646972000},"page":"185-253","source":"Crossref","is-referenced-by-count":143,"title":["Rippling: A heuristic for guiding inductive proofs"],"prefix":"10.1016","volume":"62","author":[{"given":"Alan","family":"Bundy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Stevens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"van Harmelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Ireland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0004-3702(93)90079-Q_BIB1","series-title":"Actes du Colloque Construction: Am\u00e9lioration et v\u00e9rification de Programmes","article-title":"Some generalization heuristics in proofs by induction","author":"Aubin","year":"1975"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB2","series-title":"11th Conference on Automated Deduction","first-page":"295","article-title":"Difference matching","volume":"607","author":"Basin","year":"1992"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB3","series-title":"A computational logic","author":"Boyer","year":"1979"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB4","series-title":"9th Conference on Automated Deduction","first-page":"111","article-title":"The use of explicit plans to guide inductive proofs","author":"Bundy","year":"1988"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB5","series-title":"Proceedings UK IT 90","first-page":"221","article-title":"Turning eureka steps into calculations in automatic program synthesis","author":"Bundy","year":"1990"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB6","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","article-title":"Experiments with proof plans for induction","volume":"7","author":"Bundy","year":"1991","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB7","series-title":"Proceedings IJCAI-89","first-page":"359","article-title":"A rational reconstruction and extension of recursion analysis","author":"Bundy","year":"1989"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB8","series-title":"10th International Conference on Automated Deduction","first-page":"647","article-title":"The Oyster-Clam system","volume":"449","author":"Bundy","year":"1990"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB9","series-title":"10th International Conference on Automated Deduction","first-page":"146","article-title":"Extensions to the rippling-out tactic for guiding inductive proofs","volume":"449","author":"Bundy","year":"1990"},{"issue":"2","key":"10.1016\/0004-3702(93)90079-Q_BIB10","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(81)90010-2","article-title":"Using meta-level inference for selective application of multiple rewrite rule sets in algebraic manipulation","volume":"16","author":"Bundy","year":"1981","journal-title":"Artif. Intell."},{"issue":"1","key":"10.1016\/0004-3702(93)90079-Q_BIB11","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","article-title":"A transformation system for developing recursive programs","volume":"24","author":"Burstall","year":"1977","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB12","author":"Constable","year":"1986"},{"issue":"8","key":"10.1016\/0004-3702(93)90079-Q_BIB13","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","article-title":"Proving termination with multiset orderings","volume":"22","author":"Dershowitz","year":"1979","journal-title":"Comm. ACM"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB14","article-title":"Using middle-out reasoning to guide inductive theorem proving","author":"Hesketh","year":"1991"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB15","series-title":"10th International Conference on Automated Deduction","first-page":"147","article-title":"Guiding inductive proofs","volume":"449","author":"Hutter","year":"1990"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB16","series-title":"8th Conference on Automated Deduction","first-page":"281","article-title":"Formulation of induction formulas in verification of Prolog programs","volume":"230","author":"Kanamori","year":"1986"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB17","series-title":"11th Conference on Automated Deduction","volume":"607","year":"1992"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB18","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebra","author":"Knuth","year":"1970"},{"key":"10.1016\/0004-3702(93)90079-Q_BIB19","series-title":"11th Conference on Automated Deduction","first-page":"325","article-title":"The use of proof plans to sum series","volume":"607","author":"Walsh","year":"1992"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:000437029390079Q?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:000437029390079Q?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,27]],"date-time":"2019-03-27T00:54:21Z","timestamp":1553648061000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/000437029390079Q"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,8]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,8]]}},"alternative-id":["000437029390079Q"],"URL":"https:\/\/doi.org\/10.1016\/0004-3702(93)90079-q","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1993,8]]}}}