{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:47:16Z","timestamp":1748072836365},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_175","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:19:29Z","timestamp":1330233569000},"page":"325-339","source":"Crossref","is-referenced-by-count":15,"title":["The use of proof plans to sum series"],"prefix":"10.1007","author":[{"given":"Toby","family":"Walsh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Nunes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"25_CR1","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on Automated Deduction, pages 111\u2013120, Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012826"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647\u2013648, Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303\u2013324, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, A. Smaill, and A. Ireland. Extensions to the rippling-out tactic for guiding inductive proofs. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 132\u2013146, Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_84"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"D. Basin and T. Walsh. Difference Matching. In D. Kapur, editor, 11th International Conference on Automated Deduction, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_173"},{"key":"25_CR7","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"E. Clarke and X. Zhao. Analytica \u2014 A Theorem Prover for Mathematica. Technical Report, Carnegie Mellon University, 1991.","DOI":"10.1007\/3-540-55602-8_220"},{"key":"25_CR9","unstructured":"R.W. Gosper. Indefinite hypergeometric sums in MACSYMA. In Proc. MAC-SYMA Users Conference, pages 237\u2013252, 1977."},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"D. Hutter. Guiding inductive proofs. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 147\u2013161, Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_85"},{"key":"25_CR11","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/S0747-7171(89)80007-0","volume":"7","author":"L. Sterling","year":"1989","unstructured":"L. Sterling, A. Bundy, L. Byrd, R. O'Keefe, and B. Silver. Solving symbolic equations with PRESS. J. Symbolic Computation, 7:71\u201384, 1989.","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_175.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T23:27:27Z","timestamp":1640906847000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_175"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_175","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}