{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:40:25Z","timestamp":1770277225094,"version":"3.49.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":9,"publisher":"Springer-Verlag","isbn-type":[{"value":"354019343X","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012826","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"111-120","source":"Crossref","is-referenced-by-count":146,"title":["The use of explicit plans to guide inductive proofs"],"prefix":"10.1007","author":[{"given":"Alan","family":"Bundy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series."},{"issue":"2","key":"7_CR2","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0004-3702(81)90010-2","volume":"16","author":"A. Bundy","year":"1981","unstructured":"A. Bundy and B. Welham. Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation. Artificial Intelligence, 16(2):189\u2013212, 1981. Also available as DAI Research Paper 121.","journal-title":"Artificial Intelligence"},{"key":"7_CR3","unstructured":"A. Bundy. The derivation of tactic specifications. Blue Book Note 356, Department of Artificial Intelligence, March 1987."},{"key":"7_CR4","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"7_CR5","unstructured":"R.V. Desimone. Learning control knowledge within an explanation-based learning framework. In I. Bratko and N. Lavra\u010d, editors, Progress in Machine Learning \u2014 Proceedings of 2nd European Working Session on Learning, EWSL-87, Bled, Yugoslavia, Sigma Press, May 1987. Also available as DAI Research Paper 321."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"M.J. Gordon, A.J. Milner, and C.P. Wadsworth. Edinburgh LCF \u2014 A mechanised logic of computation. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"7_CR7","unstructured":"T. B. Knoblock and R.L. Constable. Formalized metareasoning in type theory. In Proceedings of LICS, pages 237\u2013248, IEEE, 1986."},{"key":"7_CR8","unstructured":"B. Silver. Precondition analysis: learning control information. In Machine Learning 2, Tioga Publishing Company, 1984."},{"key":"7_CR9","unstructured":"A. Stevens. A Rational Reconstruction of Boyer-Moore Recursion Analysis. Research Paper forthcoming, Dept. of Artificial Intelligence, Edinburgh, 1987. submitted to ECAI-88."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012826","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:24:28Z","timestamp":1586579068000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/bfb0012826","relation":{},"subject":[]}}