{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:15:45Z","timestamp":1759637745652,"version":"3.40.5"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[2000,10]]},"DOI":"10.1023\/a:1018952121991","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"107-126","source":"Crossref","is-referenced-by-count":9,"title":["Higher order generalization and its application in program verification"],"prefix":"10.1007","volume":"28","author":[{"given":"Jianguo","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Mylopoulos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masateru","family":"Harao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masami","family":"Hagiya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"325560_CR1","first-page":"124","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"H. Barendregt, Introduction to generalized type systems, Journal of Functional Programming 1(2) (1991) 124-154.","journal-title":"Journal of Functional Programming"},{"issue":"3\/4","key":"325560_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet, The calculus of constructions, Information and Computation 76(3\/4) (1988) 95-120.","journal-title":"Information and Computation"},{"key":"325560_CR3","volume-title":"Proceedings of the 9th International Workshop on Machine Learning","author":"C. Feng","year":"1992","unstructured":"C. Feng and S. Muggleton, Towards inductive generalization in higher order logic, in: Proceedings of the 9th International Workshop on Machine Learning, eds. D. Sleeman et al. (Morgan Kaufman, San Mateo, CA, 1992)."},{"key":"325560_CR4","unstructured":"K. Furukawa, M. Imai and R. Goebel, Hyper least general generalization and its application to higher-order concept learning, Manuscript draft."},{"key":"325560_CR5","unstructured":"T.S. Gegg-Harrison, Basic Prolog schemata, CS-1989-20, Department of Computer Science, Duke University (1989)."},{"key":"325560_CR6","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0304-3975(89)90074-1","volume":"63","author":"M. Hagiya","year":"1989","unstructured":"M. Hagiya, Generalization from partial parametrization in higher order type theory, Theoretical Computer Science 63 (1989) 113-139.","journal-title":"Theoretical Computer Science"},{"key":"325560_CR7","first-page":"197","volume-title":"Proc. of ASIAN'97","author":"M. Harao","year":"1997","unstructured":"M. Harao, Proof discovery in LK system by analogy, in: Proc. of ASIAN'97, December 1997, Lecture Notes in Computer Science, Vol. 1345 (Springer, Berlin, 1997) pp. 197-211."},{"issue":"1","key":"325560_CR8","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell and G. Plotkin, A framework for defining logics, Journal of the Association for Computing Machinery 40(1) (1993) 143-184.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"325560_CR9","unstructured":"R. Hasker, The replay of program derivations, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign (1995)."},{"key":"325560_CR10","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare, An axiomatic approach to computer programming, Communications of the ACM 12 (1969).","DOI":"10.1145\/363235.363259"},{"key":"325560_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":"G.P. Huet, A unification algorithm for typed lambda calculus, Theoretical Computer Science 1 (1975) 27-57.","journal-title":"Theoretical Computer Science"},{"key":"325560_CR12","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet and B. Lang, Proving and applying program transformations expressed with second order patterns, Acta Informatica 11 (1978) 31-55.","journal-title":"Acta Informatica"},{"key":"325560_CR13","unstructured":"P. Idestam-Almquist, Generalization of Horn clauses, Ph.D. dissertation, Department of Computer Science and Systems Science, Stockholm University and the Royal Institute of Technology (1993)."},{"key":"325560_CR14","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/0304-3975(93)90004-D","volume":"113","author":"J. Lu","year":"1993","unstructured":"J. Lu and J. Xu, Analogical program derivation based on type theory, Theoretical Computer Science 113 (1993) 259-272.","journal-title":"Theoretical Computer Science"},{"key":"325560_CR15","unstructured":"J. Lu and B. Yi, An approach to analogical theorem proving, in: Automated Reasoning, IFIP Transactions A: Computer Science and Technology, Vol. 19, ed. Shi (North-Holland, Amsterdam, 1992) pp. 285-294."},{"key":"325560_CR16","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00a8of","year":"1984","unstructured":"P. Martin-L\u00a8of, Intuitionistic Type Theory, Studies in Proof Theory (Bibliopolis, Napoli, 1984)."},{"issue":"4","key":"325560_CR17","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BF03037089","volume":"8","author":"S. Muggleton","year":"1991","unstructured":"S. Muggleton, Inductive logic programming, New Generation Computing 8(4) (1991) 295-318.","journal-title":"New Generation Computing"},{"key":"325560_CR18","unstructured":"C.D. Page Jr., Anti-unification in constraint logic: foundations and applications to learnability in first order logic, to speed-up learning, and to deduction, Ph.D. dissertation, University of Illinois at Urbana-Champaign (1993)."},{"key":"325560_CR19","doi-asserted-by":"crossref","unstructured":"F. Pfenning, Unification and anti-unification in the calculus of constructions, in: Proceedings of the 6th Symposium on Logic in Computer Science (1991) pp. 74-85.","DOI":"10.1109\/LICS.1991.151632"},{"key":"325560_CR20","first-page":"153","volume":"5","author":"G.D. Plotkin","year":"1970","unstructured":"G.D. Plotkin, A note on inductive generalization, in: Machine Intelligence, Vol. 5 (Edinburgh University Press, 1970) pp. 153-163.","journal-title":"Machine Intelligence"},{"key":"325560_CR21","first-page":"101","volume":"6","author":"G.D. Plotkin","year":"1971","unstructured":"G.D. Plotkin, A further note on inductive generalization, in: Machine Intelligence, Vol. 6 (Edinburgh University Press, 1971) pp. 101-124.","journal-title":"Machine Intelligence"},{"key":"325560_CR22","first-page":"135","volume":"5","author":"J.C. Reynolds","year":"1970","unstructured":"J.C. Reynolds, Transformational systems and the algebraic structure of atomic formulas, in: Machine Intelligence, Vol. 5 (Edinburgh University Press, 1970) pp. 135-151.","journal-title":"Machine Intelligence"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018952121991.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018952121991\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018952121991.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:36:47Z","timestamp":1747546607000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018952121991"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,10]]},"references-count":22,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2000,10]]}},"alternative-id":["325560"],"URL":"https:\/\/doi.org\/10.1023\/a:1018952121991","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2000,10]]}}}