{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:05Z","timestamp":1749124085391},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105418","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"399-413","source":"Crossref","is-referenced-by-count":15,"title":["Higher-order annotated terms for proof search"],"prefix":"10.1007","author":[{"given":"Alan","family":"Smaill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Green","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"26_CR1","unstructured":"R. Aubin. Some generalization heuristics in proofs by induction. In G. Huet and G. Kahn, editors, Actes du Colloque Construction: Am\u00e9lioration et v\u00e9rification de Programmes. Institut de recherche d'informatique et d'automatique, 1975."},{"key":"26_CR2","unstructured":"H. P. Barendregt. The Lambda Calculus. Elsevier, 1985."},{"key":"26_CR3","unstructured":"David Basin and Toby Walsh. A calculus for and termination of rippling. Technical report, MPI, 1994. To appear in special issue of the Journal of Automated Reasoning."},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"David Basin and Toby Walsh. A calculus for rippling. In Proceedings of CTRS-94, 1994.","DOI":"10.1007\/3-540-60381-6_2"},{"key":"26_CR5","unstructured":"David Basin and Toby Walsh. Termination orders for rippling. In Alan Bundy, editor, 12th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 814, pages 466\u201383, Nancy, France, 1994. Springer-Verlag."},{"issue":"3","key":"26_CR6","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W.W. Bledsoe","year":"1990","unstructured":"W.W. Bledsoe. Challenge problems in elementary calculus. Journal of Automated Reasoning, 6(3):341\u2013359, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"A. Boudet and H. Comon. About the theory of tree embedding. In M.-C. Gaudek and J.-P. Jouannaud, editors, TAPSOFT\u2019 93: Theory and Practice of Software Development, number 668 in LNCS, pages 376\u201390. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56610-4_77"},{"key":"26_CR8","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. Longer version available from Edinburgh as DAI Research Paper No. 349.","DOI":"10.1007\/BFb0012826"},{"key":"26_CR9","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":"26_CR10","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":"26_CR11","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"26_CR12","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"},{"issue":"1","key":"26_CR13","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"A. Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43\u201381, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR14","unstructured":"J. K. Gallagher. The Use of Proof Plans in Tactic Synthesis. PhD thesis, University of Edinburgh, 1993."},{"issue":"1","key":"26_CR15","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1992","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u201384, 1992. Preliminary version in LICS\u2019 87.","journal-title":"Journal of the ACM"},{"key":"26_CR16","unstructured":"D. Hutter. Pattern-Direct Guidance of Equational Proofs. PhD thesis, University of Karlsruhe, 1991."},{"key":"26_CR17","unstructured":"D. Hutter and M. Kohlhase. A colored version of the \u03bb-calculus. SEKI-report sr-95-05, University of Saarland, 1995."},{"key":"26_CR18","first-page":"1","volume-title":"Handbook of Logic in Computer Science, vol 2, volume 2","author":"J.W. Klop","year":"1992","unstructured":"J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, vol 2, volume 2, pages 1\u2013116. Clarendon Press, Oxford, 1992."},{"key":"26_CR19","volume-title":"Proceedings of the 1992 Workshop on the \u03bbProlog Programming Language","author":"C. Liang","year":"1992","unstructured":"Chuck Liang. \u03bbProlog implementation of ripple-rewriting. In Proceedings of the 1992 Workshop on the \u03bbProlog Programming Language, University of Pennsylvania, Philadelphia, PA, USA, July\u2013August 1992."},{"key":"26_CR20","unstructured":"Z. Luo and R. Pollack. Lego proof development system: User's manual. Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, May 1992."},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"D. Miller. A logic programming language with lambda abstraction, function variables and simple unification. In Extensions of Logic Programming, volume 475 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1991.","DOI":"10.1093\/logcom\/1.4.497"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, pages 342\u2013349, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"26_CR23","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. Paulson","year":"1986","unstructured":"L. Paulson. Natural deduction as higher order resolution. Journal of Logic Programming, 3:237\u2013258, 1986.","journal-title":"Journal of Logic Programming"},{"key":"26_CR24","unstructured":"Alan Smaill and Ian Green. Automating the synthesis of functional programs. Research paper 777, Dept. of Artificial Intelligence, University of Edinburgh, 1995."},{"key":"26_CR25","unstructured":"Tetsuya Yoshida, Alan Bundy, Ian Green, Toby Walsh, and David Basin. Coloured rippling: An extension of a theorem proving heuristic. In A.G. Cohn, editor, In proceedings of ECAI-94, pages 85\u201389. John Wiley, 1994."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105418","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T22:52:31Z","timestamp":1639608751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105418"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0105418","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}