{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,5]],"date-time":"2024-08-05T12:38:05Z","timestamp":1722861485457},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1993,9,1]],"date-time":"1993-09-01T00:00:00Z","timestamp":746841600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1993,9]]},"DOI":"10.1007\/bf01530798","type":"journal-article","created":{"date-parts":[[2005,4,19]],"date-time":"2005-04-19T00:24:51Z","timestamp":1113870291000},"page":"363-381","source":"Crossref","is-referenced-by-count":2,"title":["A recursion planning analysis of inductive completion"],"prefix":"10.1007","volume":"8","author":[{"given":"Richard","family":"Barnett","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jane","family":"Hesketh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"R. Aubin, Some generalization heuristics in proofs by induction,Actes du Colloque Construction: Amelioration et Verification des Programmes INRIA (1975)."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair, Proofs by consistency in equational theories,Proc. LICS (1988).","DOI":"10.1109\/LICS.1988.5122"},{"key":"CR3","unstructured":"R. Barnett, An implementation and evaluation of inductive completion, MSc Thesis, University of Edinburgh (1990)."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"D. Basin and T. Walsh, Difference matching, in:Proc. 11th Int. Conf. on Automated Deduction (CADE-11), Saratoga Springs, New York, June 1992 (Springer) pp. 295?309.","DOI":"10.1007\/3-540-55602-8_173"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"S. Biundo, B. Hummel, D. Hutter and C. Walther, The Karlsruhe induction theorem proving system, in:8th Int. Conf. on Automated Deduction, Oxford, UK (1986).","DOI":"10.1007\/3-540-16780-3_132"},{"key":"CR6","unstructured":"R. Boyer and J. Moore,A Computational Logic, ACM Monograph Series (Academic Press, 1979)."},{"key":"CR7","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill and A. Stevens, A rational reconstruction and extension of recursion analysis, DAI Research Paper No. 419, University of Edinburgh (1989)."},{"key":"CR8","volume-title":"Research Paper No. 567","author":"A. Bundy","year":"1991","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, A. Ireland and A. Smaill, Rippling: A heuristic for guiding inductive proofs, Research Paper No. 567, Department of Artificial Intelligence, Edinburgh (1991). To appear in Artificial Intelligence."},{"key":"CR9","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R.M. Burstall","year":"1977","unstructured":"R.M. Burstall and J. Darlington, A transformation system for developing recursive programs, J. Assoc. Comput. Mach. 24(1977)44?67.","journal-title":"J. Assoc. Comput. Mach."},{"key":"CR10","unstructured":"N. Dershowitz, Applications of the Knuth-Bendix completion procedure,Proc. Seminaire d'Informatique Theorique (1982)."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"L. Fribourg, A strong restriction of the inductive completion procedure,Proc. ICALP 13 (1986), LNCS 226 (Springer).","DOI":"10.1007\/3-540-16761-7_60"},{"key":"CR12","unstructured":"R. G\u00f6bel, A specialized Knuth-Bendix algorithm for inductive proofs,Proc. Combinatorial Algorithms in Algebraic Structures (1985)."},{"key":"CR13","unstructured":"B. Gramlich, Inductive theorem proving using refined unfailing completion techniques, SEKI Report SR-89-14."},{"key":"CR14","unstructured":"F. van Harmelen, The Clam proof planner, Technical Report No. 4, Department of Artificial Intelligence, University of Edinburgh (1989)."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"G. Huet and J.-M. Hullot, Proofs by induction in equational theories with constructors, INRIA (1982).","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"CR16","unstructured":"J.-P. Jouannaud and E. Kornalis, Automatic proofs by induction in equational theories without constructors,Proc. LICS (1986)."},{"key":"CR17","unstructured":"W. K\u00fcchlin, Inductive completion by ground proof transformation, Technical Report No. 87-08, Department of Computer and Information Sciences, University of Delaware (1987)."},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"D.R. Musser, On proving inductive properties of abstract data types, in:ACM Symp. on Principles of Programming Languages, Las Vegas (1980) pp. 1154?1162.","DOI":"10.1145\/567446.567461"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"U. Reddy, Term rewriting induction,Proc. CADE 10 (1990), LNAI 449 (Springer).","DOI":"10.1007\/3-540-52885-7_86"},{"key":"CR20","unstructured":"A. Stevens, A rational reconstruction of Boyer and Moore's technique for constructing induction formulas,Proc. ECAI-88, Research Paper No. 360, Department of Artificial Intelligence, University of Edinburgh."},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"H. Zhang, D. Kapur and M. Krishnamoorthy, A mechanizable induction principle for equational specifications,Proc. CADE 9 (1988), LNCS 310 (Springer).","DOI":"10.1007\/BFb0012831"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01530798\/fulltext.html","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01530798.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01530798\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01530798","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T00:00:56Z","timestamp":1586217656000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01530798"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,9]]},"references-count":21,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1993,9]]}},"alternative-id":["BF01530798"],"URL":"https:\/\/doi.org\/10.1007\/bf01530798","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,9]]}}}