{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T10:12:20Z","timestamp":1771582340739,"version":"3.50.1"},"reference-count":40,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1986,10,1]],"date-time":"1986-10-01T00:00:00Z","timestamp":528508800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,19]],"date-time":"2013-07-19T00:00:00Z","timestamp":1374192000000},"content-version":"vor","delay-in-days":9788,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Journal of Logic Programming"],"published-print":{"date-parts":[[1986,10]]},"DOI":"10.1016\/0743-1066(86)90015-4","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T23:47:32Z","timestamp":1027640852000},"page":"237-258","source":"Crossref","is-referenced-by-count":98,"title":["Natural deduction as higher-order resolution"],"prefix":"10.1016","volume":"3","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0743-1066(86)90015-4_BIB1","series-title":"Frege's Formal Language","author":"Aczel","year":"1981"},{"key":"10.1016\/0743-1066(86)90015-4_BIB2","series-title":"Automated Theorem Proving: After 25 Years","first-page":"169","article-title":"Automating Higher-Order Logic","author":"Andrews","year":"1984"},{"key":"10.1016\/0743-1066(86)90015-4_BIB3","first-page":"101","article-title":"The Sharing of Structure in Theorem-Proving Programs","volume":"7","author":"Boyer","year":"1972"},{"key":"10.1016\/0743-1066(86)90015-4_BIB4","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indag. Math."},{"key":"10.1016\/0743-1066(86)90015-4_BIB5","series-title":"To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism","first-page":"579","article-title":"A Survey of the Project automath","author":"de Bruijn","year":"1980"},{"key":"10.1016\/0743-1066(86)90015-4_BIB6","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/0743-1066(86)90015-4_BIB7","series-title":"INRIA Research Report 416","article-title":"Natural Semantics on the Computer","author":"Cl\u00e9ment","year":"1985"},{"key":"10.1016\/0743-1066(86)90015-4_BIB8","first-page":"151","article-title":"Constructions: A Higher Order Proof System for Mechanizing Mathematics","volume":"203","author":"Coquand","year":"1985"},{"key":"10.1016\/0743-1066(86)90015-4_BIB9","doi-asserted-by":"crossref","DOI":"10.1007\/BF00244273","article-title":"Writing Programs That Construct Proofs","volume":"1","author":"Constable","year":"1985","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/0743-1066(86)90015-4_BIB10","first-page":"334","article-title":"Program Verification in a Logical Theory of Constructions","volume":"201","author":"Dybjer","year":"1985"},{"key":"10.1016\/0743-1066(86)90015-4_BIB11","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The Undecidability of the Second-Order Unification Problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0743-1066(86)90015-4_BIB12","series-title":"Tools and Notions for Program Construction","first-page":"163","article-title":"Representing a Logic in the lcf Metalanguage","author":"Gordon","year":"1982"},{"key":"10.1016\/0743-1066(86)90015-4_BIB13","series-title":"Report 68","article-title":"hol: A Machine Oriented Formulation of Higher Order Logic","author":"Gordon","year":"1985"},{"key":"10.1016\/0743-1066(86)90015-4_BIB14","series-title":"Report 77","article-title":"Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware","author":"Gordon","year":"1985"},{"key":"10.1016\/0743-1066(86)90015-4_BIB15","volume":"78","author":"Gordon","year":"1979"},{"key":"10.1016\/0743-1066(86)90015-4_BIB16","article-title":"A Mechanization of Type Theory","author":"Huet","year":"1973","journal-title":"Third International Joint Conference on Artificial Intelligence"},{"key":"10.1016\/0743-1066(86)90015-4_BIB17","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\/0743-1066(86)90015-4_BIB18","doi-asserted-by":"crossref","unstructured":"Huet, G.P. and Lang, B., Proving and Applying Program Transformations Expressed with Second-Order Patterns,Acta Inform. 11:31\u201355.","DOI":"10.1007\/BF00264598"},{"key":"10.1016\/0743-1066(86)90015-4_BIB19","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","article-title":"Mechanizing \u03c9-order Type Theory through Unification","volume":"3","author":"Jensen","year":"1976","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0743-1066(86)90015-4_BIB20","first-page":"65","article-title":"ekl\u2014a Mathematically Oriented Proof Checker","volume":"170","author":"Ketonen","year":"1984"},{"key":"10.1016\/0743-1066(86)90015-4_BIB21","author":"Martin-L\u00f6f","year":"1984","journal-title":"Intuitionistic Type Theory"},{"key":"10.1016\/0743-1066(86)90015-4_BIB22","series-title":"On the Meanings of the Logical Constants and the Justifications of the Logical Laws","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/0743-1066(86)90015-4_BIB23","series-title":"Seventh Conference on Automated Deduction","first-page":"375","article-title":"Expansion tree proofs and their conversion to natural deduction proofs","author":"Miller","year":"1984"},{"key":"10.1016\/0743-1066(86)90015-4_BIB24","series-title":"Sixth Conference on Automated Deduction","first-page":"50","article-title":"A Look at tps","author":"Miller","year":"1982"},{"key":"10.1016\/0743-1066(86)90015-4_BIB25","doi-asserted-by":"crossref","DOI":"10.1016\/0022-0000(78)90014-4","article-title":"A Theory of Type Polymorphism in Programming","volume":"17","author":"Milner","year":"1978","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/0743-1066(86)90015-4_BIB26","first-page":"184","article-title":"A Proposal for Standard ml","author":"Milner","year":"1984","journal-title":"ACM Symposium on Lisp and Functional Programming"},{"key":"10.1016\/0743-1066(86)90015-4_BIB27","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1098\/rsta.1984.0067","article-title":"The Use of Machines to Assist in Rigorous Proof","volume":"312","author":"Milner","year":"1984","journal-title":"Philos. Trans. Roy. Soc. London"},{"key":"10.1016\/0743-1066(86)90015-4_BIB28","series-title":"Ph.D. Thesis","article-title":"Data Type Proofs Using Edinburgh lcf","author":"Monahan","year":"1984"},{"key":"10.1016\/0743-1066(86)90015-4_BIB29","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/BF02136027","article-title":"Propositions and Specifications of Programs in Martin-L\u00f6f's Type Theory","volume":"24","author":"Nordstr\u00f6m","year":"1984","journal-title":"BIT"},{"key":"10.1016\/0743-1066(86)90015-4_BIB30","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Lessons Learned from lcf: A Survey of Natural Deduction Proofs, Comput. J. 28, to appear.","DOI":"10.1093\/comjnl\/28.5.474"},{"key":"10.1016\/0743-1066(86)90015-4_BIB31","series-title":"Report 80","article-title":"Interactive Theorem Proving with Cambridge lcf: A User's Manual","author":"Paulson","year":"1985"},{"key":"10.1016\/0743-1066(86)90015-4_BIB32","series-title":"Report 21","article-title":"A Programming System for Type Theory","author":"Peterson","year":"1982"},{"key":"10.1016\/0743-1066(86)90015-4_BIB33","series-title":"Logic: Form and Function","author":"Robinson","year":"1979"},{"key":"10.1016\/0743-1066(86)90015-4_BIB34","series-title":"Report CSR-142-83","article-title":"Natural Deduction Theorem Proving in Set Theory","author":"Schmidt","year":"1983"},{"key":"10.1016\/0743-1066(86)90015-4_BIB35","series-title":"Seventh Conference on Automated Deduction","first-page":"445","article-title":"A Programming Notation for Tactical Reasoning","author":"Schmidt","year":"1984"},{"key":"10.1016\/0743-1066(86)90015-4_BIB36","series-title":"Report CSR-140-83","article-title":"A Note on Tactics in lcf","author":"Sokolowski","year":"1983"},{"key":"10.1016\/0743-1066(86)90015-4_BIB37","series-title":"Report CSR-146-83","article-title":"An lcf Proof of the Soundness of Hoare's Logic","author":"Sokolowski","year":"1983"},{"key":"10.1016\/0743-1066(86)90015-4_BIB38","series-title":"Natural Logic","author":"Tennant","year":"1978"},{"key":"10.1016\/0743-1066(86)90015-4_BIB39","series-title":"Research paper 258","article-title":"Generating Connection Calculi from Tableaux and Sequent Based Proof Systems","author":"Wallen","year":"1985"},{"key":"10.1016\/0743-1066(86)90015-4_BIB40","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-15976-2_23","article-title":"The Set of Unifiers in Typed \u03bb-calculus as Regular Expressions","author":"Zaionc","year":"1985","journal-title":"Rewriting Techniques and Applications"}],"container-title":["The Journal of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0743106686900154?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0743106686900154?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,5]],"date-time":"2020-02-05T06:25:48Z","timestamp":1580883948000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0743106686900154"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986,10]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1986,10]]}},"alternative-id":["0743106686900154"],"URL":"https:\/\/doi.org\/10.1016\/0743-1066(86)90015-4","relation":{},"ISSN":["0743-1066"],"issn-type":[{"value":"0743-1066","type":"print"}],"subject":[],"published":{"date-parts":[[1986,10]]}}}