{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:22Z","timestamp":1761611182835},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054254","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"129-133","source":"Crossref","is-referenced-by-count":23,"title":["System description: Proof planning in higher-order logic with \u03bbClam"],"prefix":"10.1007","author":[{"given":"Julian","family":"Richardson","sequence":"first","affiliation":[]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Green","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"15_CR1","volume-title":"The architecture of an implementation of LambdaProlog: Prolog\/Mali","author":"P. Brisset","year":"1994","unstructured":"P. Brisset and O. Ridoux. The architecture of an implementation of LambdaProlog: Prolog\/Mali. In Proceedings of the Workshop on Implementation of Logic Programming, ILPS'94, Ithaca, NY. The MIT Press, November 1994."},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185\u2013253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artificial Intelligence"},{"key":"15_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. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Alan 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. Longer version available as DAI Research Paper No. 349.","DOI":"10.1007\/BFb0012819"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"A. Felty. A logic programming approach to implementing higher-order term rewriting. In L-H Eriksson et al., editors, Second International Workshop on Extensions to Logic Programming, volume 596 of Lecture Notes in Artificial Intelligence, pages 135\u201361. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0013606"},{"key":"15_CR6","unstructured":"J. T. Hesketh. Using Middle-Out Reasoning to Guide Inductive Theorem Proving. PhD thesis, University of Edinburgh, 1991."},{"issue":"1\u20132","key":"15_CR7","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1\u20132):79\u2013111, 1996. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"A. Smaill and I. Green. Higher-order annotated terms for proof search. In J. von Wright, J. Grundy, and J Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 399\u2013414. Springer, 1996. Also available as DAI Research Paper 799.","DOI":"10.1007\/BFb0105418"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054254","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,10]],"date-time":"2019-02-10T22:06:28Z","timestamp":1549836388000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054254"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0054254","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}