{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:26Z","timestamp":1749124046851},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1991,9,1]],"date-time":"1991-09-01T00:00:00Z","timestamp":683683200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1991,9]]},"DOI":"10.1007\/bf00249016","type":"journal-article","created":{"date-parts":[[2004,10,3]],"date-time":"2004-10-03T22:38:26Z","timestamp":1096843106000},"page":"303-324","source":"Crossref","is-referenced-by-count":66,"title":["Experiments with proof plans for induction"],"prefix":"10.1007","volume":"7","author":[{"given":"Alan","family":"Bundy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"van Harmelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jane","family":"Hesketh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Aubin, R., ?Some generalization heuristics in proofs by induction?. In Actes du Colloque Construction: Amelioration et verification de Programmes, Institut de recherche d'informatique et d'automatique, 1975."},{"key":"CR2","unstructured":"Boyer, R. S. and Moore, J S., A Computational Logic, Academic Press, 1979, ACM monograph series."},{"issue":"1","key":"CR3","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BF00244511","volume":"4","author":"A. Bundy","year":"1988","unstructured":"Bundy, A. and Sterling, L. S., ?Meta-level inference: two application?, Journal of Automated Reasoning 4(1), 15?27 (1988). Also available from Edinburgh, Dept. of AI, as Research Paper No. 273.","journal-title":"Journal of Automated Reasoning"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Bundy, A., ?The use of explicit plans to guide inductive proofs?. In 9th Conference on Automated Deduction, pages 111?120, Springer-Verlag, 1988. Longer version available as DAI Research Paper No. 349.","DOI":"10.1007\/BFb0012826"},{"key":"CR5","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A. and Stevens, A., ?A Rational Reconstruction and Extension of Recursion Analysis?, Proc. of IJCAI-89 (Sridharan, ed.), Morgan Kaufmann, 1989, 359?365."},{"issue":"1","key":"CR6","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. M. Burstall","year":"1977","unstructured":"Burstall, R. M. and Darlington, J., ?A transformation system for developing recursive programs?. Journal of the ACM 24(1), 44?67 (1977).","journal-title":"Journal of the ACM"},{"key":"CR7","unstructured":"Constable, R. L., Allen, S. F., Bromley, H. M. et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"CR8","unstructured":"Desimone, R. V., ?Explanation-based learning of proof plans?. In Y. Kodratoff (Ed.) Machine and Human Learning, Ellis Horwood, 1987. Also available as DAI Research Paper 304. Previous version in proceedings of EWSL-86."},{"key":"CR9","unstructured":"Gallaire, H. and Lasserre, C., ?Metalevel control for logic programs?. In Logic Programming, p. 173?185, Academic Press, 1982."},{"key":"CR10","unstructured":"Giunchiglia, F. and Walsh, T., ?Abstract Theorem Proving?. Proc. of IJCAI-89 (Shridharan, ed.), Morgan Kaufmann, 1989, pp. 372?377."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Gordon, M. J., Milner, A. J. and Wadsworth, C. P., Edinburgh LCF-A mechanised logic of computation. Volume 78 of Lecture Notes in Computer Science, Springer Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"CR12","unstructured":"Horn, C., The Nur PRL Proof Development System. Working paper 214, Dept. of Artificial Intelligence, Edinburgh, 1988. The Edinburgh version of NurPRL has been renamed Oyster."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Kanamori, T. and Fujita, H., ?Formulation of induction formulas in verification of Prolog programs. In 8th Conference on Automated Deduction, p. 281?299, Springer-Verlag, 1986. Springer Lecture Notes in Computer Science No. 230.","DOI":"10.1007\/3-540-16780-3_97"},{"key":"CR14","unstructured":"Knoblock, T. B. and Constable, R. L., ?Formalized metareasoning in type theory?. In Proceedings of LICS, p. 237?248, IEEE, 1986."},{"key":"CR15","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"6th International Congress for Logic, Methodology and Philosophy of Science","author":"Per Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, Per, ?Constructive mathematics and computer programming?. In 6th International Congress for Logic, Methodology and Philosophy of Science, p. 153?175, Hanover, August 1979. Published by North Holland, Amsterdam, 1982."},{"key":"CR16","unstructured":"Paulson, L., ?Experience with Isabelle: a generic theorem prover?. In COLOG 88, Institute of Cybernetics of the Estonian SSR, 1988."},{"key":"CR17","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0004-3702(74)90026-5","volume":"5","author":"E. D. Sacerdoti","year":"1974","unstructured":"Sacerdoti, E. D., ?Planning in a hierarchy of a abstraction spaces?. Artificial Intelligence 5, 115?135 (1974).","journal-title":"Artificial Intelligence"},{"key":"CR18","unstructured":"Silver, B., Meta-Level Inference: Representing and Learning Control Information in Artificial Intelligence. North Holland, 1985. Revised version of the author's PhD thesis, DAI 1984."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00249016.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00249016\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00249016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T15:56:00Z","timestamp":1554306960000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00249016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,9]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1991,9]]}},"alternative-id":["BF00249016"],"URL":"https:\/\/doi.org\/10.1007\/bf00249016","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,9]]}}}