{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T15:46:11Z","timestamp":1648827971658},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,5,13]],"date-time":"2010-05-13T00:00:00Z","timestamp":1273708800000},"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":[[2011,6]]},"DOI":"10.1007\/s10817-010-9177-y","type":"journal-article","created":{"date-parts":[[2010,5,12]],"date-time":"2010-05-12T08:26:53Z","timestamp":1273652813000},"page":"57-105","source":"Crossref","is-referenced-by-count":0,"title":["The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling"],"prefix":"10.1007","volume":"47","author":[{"given":"Louise Abigail","family":"Dennis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Green","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,5,13]]},"reference":[{"issue":"1\u20132","key":"9177_CR1","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D Basin","year":"1996","unstructured":"Basin, D., Walsh, T.: A calculus for and termination of rippling. J. Autom. Reason. 16(1\u20132), 147\u2013180 (1996)","journal-title":"J. Autom. Reason."},{"key":"9177_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/3-540-56610-4_77","volume-title":"TAPSOFT \u201993: Theory and Practice of Software Development","author":"A Boudet","year":"1993","unstructured":"Boudet, A., Comon, H.: About the theory of tree embedding. In: Gaudek, M.-C., Jouannaud, J.-P. (eds.) TAPSOFT \u201993: Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 668, pp. 376\u2013390. Springer, Berlin (1993)"},{"key":"9177_CR3","first-page":"178","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"A Bundy","year":"1991","unstructured":"Bundy, A.: A science of reasoning. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 178\u2013198. MIT, Cambridge (1991)"},{"key":"9177_CR4","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: Meta-Level Guidance for Mathematical Reasoning","author":"A Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol. 56. Cambridge University Press, Cambridge (2005)"},{"key":"9177_CR5","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62, 185\u2013253 (1993, Also available from Edinburgh as DAI Research Paper No. 567)","journal-title":"Artif. Intell."},{"key":"9177_CR6","unstructured":"Dennis, L.A.: Program slicing and middle-out reasoning for error location and repair. In: Disproving: Non-Theorems, Non-Validity and Non-Provability (2006)"},{"key":"9177_CR7","unstructured":"Dennis, L.A., Brotherston, J.: \u03bbclam v4: User\/Developer\u2019s Manual. Mathematical Reasoning Group, Division of Informatics, University of Edinburgh, Edinburgh (2002)"},{"key":"9177_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-44755-5_14","volume-title":"Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001","author":"LA Dennis","year":"2001","unstructured":"Dennis, L.A., Smaill, A.: Ordinal arithmetic: a case study for rippling in a higher order domain. In: Boulton, R.J., Jackson, P.B. (eds.) Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001. Lecture Notes in Computer Science, vol. 2152, pp. 185\u2013200. Springer, Berlin (2001)"},{"key":"9177_CR9","doi-asserted-by":"crossref","unstructured":"Dixon, L., Fleuriot, J.D.: Higher order rippling in IsaPlanner. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 3223, pp. 83\u201398 (2004)","DOI":"10.1007\/978-3-540-30142-4_7"},{"key":"9177_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BFb0013606","volume-title":"Second International Workshop on Extensions to Logic Programming","author":"A Felty","year":"1992","unstructured":"Felty, A.: A logic programming approach to implementing higher-order term rewriting. In: Eriksson, L.-H., et al. (eds.) Second International Workshop on Extensions to Logic Programming. Lecture Notes in Computer Science, vol. 596, pp. 135\u201361. Springer, Berlin (1992)"},{"key":"9177_CR11","unstructured":"Gallagher, J.K.: The use of proof plans in tactic synthesis. Ph.D. thesis, University of Edinburgh (1993)"},{"key":"9177_CR12","first-page":"1","volume-title":"Proceedings of the Thirty-Fourth Annual Meeting of the Association for Computational Linguistics","author":"C Gardent","year":"1996","unstructured":"Gardent, C., Kohlhase, M.: Higher-order coloured unification and natural language semantics. In: Joshi, A., Palmer, M. (eds.) Proceedings of the Thirty-Fourth Annual Meeting of the Association for Computational Linguistics, pp. 1\u20139. Morgan Kaufmann, San Francisco (1996)"},{"key":"9177_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-52885-7_85","volume-title":"10th International Conference on Automated Deduction","author":"D Hutter","year":"1990","unstructured":"Hutter, D.: Guiding inductive proofs. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 449, pp. 147\u2013161. Springer, Berlin (1990)"},{"key":"9177_CR14","unstructured":"Hutter, D.: Pattern-direct guidance of equational proofs. Ph.D. thesis, University of Karlsruhe (1991)"},{"key":"9177_CR15","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings 20th German Annual Conference on Artificial Intelligence KI-96","author":"D Hutter","year":"1996","unstructured":"Hutter, D.: Using rippling for equational reasoning. In: H\u00f6lldobler, S. (ed.) Proceedings 20th German Annual Conference on Artificial Intelligence KI-96. Lecture Notes in Artificial Intelligence, vol. 1137. Springer, Berlin (1996)"},{"issue":"2","key":"9177_CR16","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1023\/A:1006282725324","volume":"25","author":"D Hutter","year":"2000","unstructured":"Hutter, D., Kohlhase, M.: Managing structural information by higher-order colored unification. J. Autom. Reason. 25(2), 123\u2013164 (2000)","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"9177_CR17","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reason. 16(1\u20132), 79\u2013111 (1996, Also available from Edinburgh as DAI Research Paper No. 716)","journal-title":"J. Autom. Reason."},{"key":"9177_CR18","volume-title":"Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming","author":"J-P Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Okada, M.: Satisfiability of systems of ordinal notations with the subterm property is decidable. In: Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming. Madrid, Spain (1991)"},{"key":"9177_CR19","first-page":"1","volume-title":"Handbook of Logic in Computer Science, vol. 2","author":"JW Klop","year":"1992","unstructured":"Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D., Maibaum, T.S. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 1\u2013116. Clarendon, Oxford (1992)"},{"key":"9177_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Computational Logic\u2014CL2000","author":"D Lacey","year":"2000","unstructured":"Lacey, D., Richardson, J., Smaill, A.: Logic program synthesis in a higher-order setting. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) Computational Logic\u2014CL2000. Lecture Notes in Computer Science, vol. 1861. Springer, Berlin (2000)"},{"key":"9177_CR21","volume-title":"Proceedings of the 1992 Workshop on the \u03bbProlog Programming Language","author":"C Liang","year":"1992","unstructured":"Liang, C.: \u03bbProlog implementation of ripple-rewriting. In: Proceedings of the 1992 Workshop on the \u03bbProlog Programming Language. University of Pennsylvania, Philadelphia (1992)"},{"key":"9177_CR22","unstructured":"Luo, Z., Pollack, R.: LEGO Proof Development System: User\u2019s Manual. Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, Edinburgh (1992)"},{"key":"9177_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46406-9","volume-title":"Computation Logic (CL\u20192000)","author":"D Miller","year":"2000","unstructured":"Miller, D.: Abstract syntax for variable binders: an overview. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) Computation Logic (CL\u20192000). Lecture Notes in Computer Science, vol. 1861. Springer, Berlin (2000)"},{"key":"9177_CR24","unstructured":"Negrete, S., Smaill, A.: Guiding proof search in logical frameworks with rippling. Technical Report, Dept. of Artificial Intelligence, University of Edinburgh, Edinburgh (1995)"},{"key":"9177_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 823. Springer, Berlin (1994)"},{"key":"9177_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BFb0054254","volume-title":"Conference on Automated Deduction (CADE\u201998)","author":"J Richardson","year":"1998","unstructured":"Richardson, J., Smaill, A., Green, I.: System description: proof planning in higher-order logic with Lambda-Clam. In: Kirchner, C., Kirchner, H. (eds.) Conference on Automated Deduction (CADE\u201998). Lecture Notes in Computer Science, vol. 1421, pp. 129\u2013133. Springer, Berlin (1998)"},{"key":"9177_CR27","unstructured":"Smaill, A., Green, I.: Automating the Synthesis of Functional Programs. Research paper 777, Dept. of Artificial Intelligence, University of Edinburgh, Edinburgh (1995)"},{"key":"9177_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BFb0105418","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"A Smaill","year":"1996","unstructured":"Smaill, A., Green, I.: Higher-order annotated terms for proof search. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996. Lecture Notes in Computer Science, vol. 1275, pp. 399\u2013414. Springer, Berlin (1996, Also available as DAI Research Paper 799)"},{"key":"9177_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/3-540-55602-8_175","volume-title":"CADE11","author":"T Walsh","year":"1992","unstructured":"Walsh, T., Nunes, A., Bundy, A.: The use of proof plans to sum series. In: Kapur, D. (ed.) CADE11. Lecture Notes in Computer Science, vol. 607, pp. 325\u2013339. Springer, Berlin (1992)"},{"key":"9177_CR30","first-page":"85","volume-title":"Proceedings of ECAI-94","author":"T Yoshida","year":"1994","unstructured":"Yoshida, T., Bundy, A., Green, I., Walsh, T., Basin, D.: Coloured rippling: an extension of a theorem proving heuristic. In: Cohn, A.G. (ed.) Proceedings of ECAI-94, pp. 85\u201389. Wiley, New York (1994)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9177-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9177-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9177-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:50Z","timestamp":1559265710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9177-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,13]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["9177"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9177-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5,13]]}}}