{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:15:07Z","timestamp":1759637707373},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_56","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:46:38Z","timestamp":1330209998000},"page":"387-419","source":"Crossref","is-referenced-by-count":3,"title":["From programming-by-example to proving-by-example"],"prefix":"10.1007","author":[{"given":"Masami","family":"Hagiya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"3","key":"19_CR1","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/356914.356918","volume":"15","author":"D. Angluin","year":"1983","unstructured":"Angluin, D., Smith, C. H.: Inductive inference: Theory and methods, Computing Surveys, Vol.15, No.3 (1983), pp.237\u2013269.","journal-title":"Computing Surveys"},{"key":"19_CR2","unstructured":"Barendregt, H.: Introduction to generalized type systems, Theoretical Computer Science \u2014 Proceedings of the Third Italian Conference, World Scientific, 1989, pp.1\u201337."},{"key":"19_CR3","unstructured":"Dybjer, P.: An inversion principle for Martin-L\u00f6f's type theory, Proceedings of the Workshop on Programming Logic, PMG-R54, University of G\u00f6teborg and Chalmers University of Technology, 1989, pp.177\u2013188."},{"key":"19_CR4","unstructured":"Elliott, C. M.: Higher-order unification with dependent function types, Rewriting Techniques and Applications (Dershowitz, N. ed.), LNCS355 (1989), pp.121\u2013136."},{"key":"19_CR5","unstructured":"Elliott, C. M.: Some extensions and applications of higher-order unification, Ph.D Thesis, School of Computer Science, Carnegie Mellon University, 1990."},{"issue":"2","key":"19_CR6","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/66443.66445","volume":"21","author":"T. Ellman","year":"1989","unstructured":"Ellman, T.: Explanation-based learning: A survey of programs and perspectives, ACM Computing Surveys, Vol.21, No.2 (1989), pp.163\u2013221.","journal-title":"ACM Computing Surveys"},{"key":"19_CR7","unstructured":"Hagiya, M.: Programming by example and proving by example using higher-order unification, 10th International Conference on Automated Deduction, LNAI449 (1990), pp.588\u2013602."},{"issue":"4","key":"19_CR8","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/BF03037096","volume":"8","author":"M. Hagiya","year":"1991","unstructured":"Hagiya, M.: Synthesis of rewrite programs by higher-order and semantic unification, Proceedings of the First International Workshop on Algorithmic Learning Theory (1990), pp.396\u2013410. Also in New Generation Computing, Vol.8, No.4 (1991), pp.403\u2013420.","journal-title":"Also in New Generation Computing"},{"key":"19_CR9","unstructured":"Hagiya, M.: On reduction and projection in type theory with inductive definitions, in preparation."},{"key":"19_CR10","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics, Symposium on Logic in Computer Science, 1987, pp.194\u2013204."},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"Huet, G. P.: A unification algorithm for typed \u03bb-calculus, Theoretical Computer Science, Vol.1 (1975), pp.27\u201357.","journal-title":"Theoretical Computer Science"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns, Acta Informatica, Vol.11 (1978), pp.31\u201355.","journal-title":"Acta Informatica"},{"issue":"7","key":"19_CR13","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/BF00995500","volume":"8","author":"Y. Kodratoff","year":"1979","unstructured":"Kodratoff, Y.: A class of functions synthesized from a finite number of examples and a LISP program scheme, International Journal of Computer and Information Science, Vol.8, Nol.7 (1979), pp.489\u2013521.","journal-title":"International Journal of Computer and Information Science"},{"key":"19_CR14","first-page":"332","volume":"4","author":"X. Ling","year":"1989","unstructured":"Ling, X.: Inventing theoretical terms in inductive learning of functions \u2014 search and constructive methods, Methodologies for Intelligent Systems (Ras, Z. W. ed.), Vol.4 (1989), pp.332\u2013341.","journal-title":"Methodologies for Intelligent Systems"},{"key":"19_CR15","first-page":"236","volume":"87","author":"J. W. Shavlik","year":"1987","unstructured":"Shavlik, J. W., DeJong, G. F.: An explanation-based approach to generalizing number, Proceedings of IJCAI 87, 1987, pp.236\u2013238.","journal-title":"Proceedings of IJCAI"},{"issue":"1&2","key":"19_CR16","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"Snyder, W., Gallier, J.: Higher-order unification revisited: Complete sets of transformations, Journal of Symbolic Computation, Vol.8, Nos 1&2 (1989), pp.101\u2013140.","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"19_CR17","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1145\/321992.322002","volume":"24","author":"P.D. Summers","year":"1977","unstructured":"Summers, P.D.: A methodology for LISP program construction from examples, Journal of ACM, Vol.24, No.1 (1977), pp.161\u2013175.","journal-title":"Journal of ACM"},{"key":"19_CR18","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1016\/0004-3702(88)90088-4","volume":"36","author":"F. Harmelen Van","year":"1988","unstructured":"Van Harmelen, F., Bundy, A.: Explanation-based generalization = partial evaluation, Artificial Intelligence, Vol.36 (1988), pp.401\u2013412.","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_56.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:21:27Z","timestamp":1619572887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}