@article{AIJ92,
  title = {{Rippling: A Heuristic for Guiding Inductive Proofs}},
  author = {Alan Bundy and Andrew Stevens and Andrew Ireland and
           Frank van Harmelen and Alan Smaill},
  issn = {00043702},
  journal = {Artificial Intelligence},
  number = {2},
  volume = {62},
  pages = {185--253},
  keywords = {Automated Reasoning},
  institution = {Department of AI, University of Edinburgh},
  url = {http://www.cs.vu.nl/~frankh/postscript/AIJ92.pdf},
  year = {1993},
  abstract = {We describe rippling: a tactic for the heuristic control of
    the key part of proofs by mathematical induction. This tactic
    significantly reduces the search for a proof of a wide variety of
    inductive theorems. We first present a basic version of rippling,
    followed by various extensions which are necessary to capture larger
    classes of inductive proofs. Finally, we present a generalised form
    of rippling which embodies these extensions as special cases. We
    prove that generalised rippling always terminates, and we discuss
    the implementation of the tactic and its relation with other
    inductive proof search heuristics.},
}

{"_id":"27ZrKuhaQAwbasYLF","bibbaseid":"bundy-stevens-ireland-vanharmelen-smaill-ripplingaheuristicforguidinginductiveproofs-1993","author_short":["Bundy, A.","Stevens, A.","Ireland, A.","van Harmelen, F.","Smaill, A."],"bibdata":{"bibtype":"article","type":"article","title":"Rippling: A Heuristic for Guiding Inductive Proofs","author":[{"firstnames":["Alan"],"propositions":[],"lastnames":["Bundy"],"suffixes":[]},{"firstnames":["Andrew"],"propositions":[],"lastnames":["Stevens"],"suffixes":[]},{"firstnames":["Andrew"],"propositions":[],"lastnames":["Ireland"],"suffixes":[]},{"firstnames":["Frank"],"propositions":["van"],"lastnames":["Harmelen"],"suffixes":[]},{"firstnames":["Alan"],"propositions":[],"lastnames":["Smaill"],"suffixes":[]}],"issn":"00043702","journal":"Artificial Intelligence","number":"2","volume":"62","pages":"185–253","keywords":"Automated Reasoning","institution":"Department of AI, University of Edinburgh","url":"http://www.cs.vu.nl/~frankh/postscript/AIJ92.pdf","year":"1993","abstract":"We describe rippling: a tactic for the heuristic control of the key part of proofs by mathematical induction. This tactic significantly reduces the search for a proof of a wide variety of inductive theorems. We first present a basic version of rippling, followed by various extensions which are necessary to capture larger classes of inductive proofs. Finally, we present a generalised form of rippling which embodies these extensions as special cases. We prove that generalised rippling always terminates, and we discuss the implementation of the tactic and its relation with other inductive proof search heuristics.","bibtex":"@article{AIJ92,\r\n title = {{Rippling: A Heuristic for Guiding Inductive Proofs}},\r\n author = {Alan Bundy and Andrew Stevens and Andrew Ireland and\r\n Frank van Harmelen and Alan Smaill},\r\n issn = {00043702},\r\n journal = {Artificial Intelligence},\r\n number = {2},\r\n volume = {62},\r\n pages = {185--253},\r\n keywords = {Automated Reasoning},\r\n institution = {Department of AI, University of Edinburgh},\r\n url = {http://www.cs.vu.nl/~frankh/postscript/AIJ92.pdf},\r\n year = {1993},\r\n abstract = {We describe rippling: a tactic for the heuristic control of\r\n the key part of proofs by mathematical induction. This tactic\r\n significantly reduces the search for a proof of a wide variety of\r\n inductive theorems. We first present a basic version of rippling,\r\n followed by various extensions which are necessary to capture larger\r\n classes of inductive proofs. Finally, we present a generalised form\r\n of rippling which embodies these extensions as special cases. We\r\n prove that generalised rippling always terminates, and we discuss\r\n the implementation of the tactic and its relation with other\r\n inductive proof search heuristics.},\r\n}\r\n\r\n","author_short":["Bundy, A.","Stevens, A.","Ireland, A.","van Harmelen, F.","Smaill, A."],"key":"AIJ92","id":"AIJ92","bibbaseid":"bundy-stevens-ireland-vanharmelen-smaill-ripplingaheuristicforguidinginductiveproofs-1993","role":"author","urls":{"Paper":"http://www.cs.vu.nl/~frankh/postscript/AIJ92.pdf"},"keyword":["Automated Reasoning"],"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"article","biburl":"http://www.cs.vu.nl/~frankh/abstracts/all.bib","dataSources":["9CnmDh6oPMNTwHksm"],"keywords":["automated reasoning"],"search_terms":["rippling","heuristic","guiding","inductive","proofs","bundy","stevens","ireland","van harmelen","smaill"],"title":"Rippling: A Heuristic for Guiding Inductive Proofs","year":1993}