{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:03:14Z","timestamp":1760061794300},"reference-count":25,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1976,11,1]],"date-time":"1976-11-01T00:00:00Z","timestamp":215654400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":13407,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1976,11]]},"DOI":"10.1016\/0304-3975(76)90021-9","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T04:17:21Z","timestamp":1027657041000},"page":"123-171","source":"Crossref","is-referenced-by-count":42,"title":["Mechanizing \u03c9-order type theory through unification"],"prefix":"10.1016","volume":"3","author":[{"given":"D.C.","family":"Jensen","sequence":"first","affiliation":[]},{"given":"T.","family":"Pietrzykowski","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(76)90021-9_BIB1","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","article-title":"Resolution in type theory","volume":"36","author":"Andrews","year":"1971","journal-title":"J Symbolic Logic"},{"key":"10.1016\/0304-3975(76)90021-9_BIB2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(76)90021-9_BIB3","first-page":"113","article-title":"Automatic theorem proving with equality substitutions and mathematical induction","volume":"3","author":"Darlington","year":"1968"},{"key":"10.1016\/0304-3975(76)90021-9_BIB4","first-page":"91","article-title":"A partial mechanization of second-order logic","volume":"6","author":"Darlington","year":"1971"},{"key":"10.1016\/0304-3975(76)90021-9_BIB5","article-title":"A matching procedure for omega-order logic","author":"Gould","year":"1966"},{"key":"10.1016\/0304-3975(76)90021-9_BIB6","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"15","author":"Henkin","year":"1950","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(76)90021-9_BIB7","article-title":"Constrained resolution: A complete method for higher order logic","author":"Huet","year":"1972"},{"key":"10.1016\/0304-3975(76)90021-9_BIB8","article-title":"A mechanization of type theory","author":"Huet","year":"1973","journal-title":"Institut de Recherche d'Informatique et d'Automatique"},{"issue":"3","key":"10.1016\/0304-3975(76)90021-9_BIB9","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","article-title":"The undecidability of unification in third-order logic","volume":"22","author":"Huet","year":"1973","journal-title":"Information and Control"},{"key":"10.1016\/0304-3975(76)90021-9_BIB10","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(76)90021-9_BIB11","article-title":"A two-valued type theory model convenient for resolution theorem proving","author":"Jensen","year":"1971"},{"key":"10.1016\/0304-3975(76)90021-9_BIB12","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/malq.19680140702","article-title":"Reflection principles and their use for establishing the complexity of axiom systems","volume":"14","author":"Kreisel","year":"1968","journal-title":"Z. Math. Logik"},{"key":"10.1016\/0304-3975(76)90021-9_BIB13","article-title":"The undecidability of the unification for third-order languages","author":"Lucchesi","year":"1972"},{"key":"10.1016\/0304-3975(76)90021-9_BIB14","author":"Monk","year":"1969"},{"key":"10.1016\/0304-3975(76)90021-9_BIB15","first-page":"287","article-title":"E-resolution: extension of resolution to include the equality relation","author":"Morris","year":"1969","journal-title":"Proc. of Int. Joint Conf. on Artificial Intelligence"},{"issue":"2","key":"10.1016\/0304-3975(76)90021-9_BIB16","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/321752.321764","article-title":"A complete mechanization of second-order type theory","volume":"20","author":"Pietrzykowski","year":"1973","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(76)90021-9_BIB17","first-page":"82","article-title":"A complete mechanization of omega-order type theory","volume":"Vol II","author":"Pietrzykowski","year":"1972","journal-title":"Proc. ACM Conference"},{"issue":"1","key":"10.1016\/0304-3975(76)90021-9_BIB18","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(76)90021-9_BIB19","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"Internatl. J. Comput. Math."},{"key":"10.1016\/0304-3975(76)90021-9_BIB20","first-page":"113","article-title":"The generalized resolution principle","volume":"3","author":"Robinson","year":"1968"},{"key":"10.1016\/0304-3975(76)90021-9_BIB21","first-page":"63","article-title":"New directions in mechanical theorem proving","volume":"Vol. I","author":"Robinson","year":"1969"},{"key":"10.1016\/0304-3975(76)90021-9_BIB22","first-page":"157","article-title":"Mechanizing higher-order logic","volume":"4","author":"Robinson","year":"1969"},{"key":"10.1016\/0304-3975(76)90021-9_BIB23","first-page":"121","article-title":"A note on mechanizing higher-order logic","volume":"5","author":"Robinson","year":"1970"},{"key":"10.1016\/0304-3975(76)90021-9_BIB24","first-page":"135","article-title":"Paramodulation and theorem proving in first-order theories with equality","volume":"4","author":"Robinson","year":"1969"},{"key":"10.1016\/0304-3975(76)90021-9_BIB25","author":"Shoenfield","year":"1967"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397576900219?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397576900219?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T13:54:17Z","timestamp":1555077257000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397576900219"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1976,11]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1976,11]]}},"alternative-id":["0304397576900219"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(76)90021-9","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1976,11]]}}}