{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T15:14:17Z","timestamp":1772032457843,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1989,9,1]],"date-time":"1989-09-01T00:00:00Z","timestamp":620611200000},"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":[[1989,9]]},"DOI":"10.1007\/bf00248324","type":"journal-article","created":{"date-parts":[[2004,10,5]],"date-time":"2004-10-05T13:40:08Z","timestamp":1096983608000},"page":"363-397","source":"Crossref","is-referenced-by-count":194,"title":["The foundation of a generic theorem prover"],"prefix":"10.1007","volume":"5","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"Andrews, P. B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press (1986)."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Andrews, P. B., Miller, D. A., Cohen, E. L., and Pfenning, F.: ?Automating higher-order logic?, in: Bledsoe, W. W. and Loveland, D. W. (eds.) Automated Theorem Proving: After 25 Years, American Mathematical Society (1984) pp. 169?192.","DOI":"10.1090\/conm\/029\/09"},{"key":"CR3","unstructured":"Avron, A., Honsell, F. A., and Mason, I. A.: ?Using typed lambda calculus to implement formal systems on a machine.? Report ECS-LFCS-87-31, Computer Science Department, University of Edinburgh (1987)."},{"key":"CR4","unstructured":"Barwise, J. (ed.): Handbook of Mathematical Logic, North-Holland (1977)."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Barwise, J.: ?An introduction to first-order logic?, in: Barwise [4], pp. 5?46.","DOI":"10.1016\/S0049-237X(08)71097-8"},{"key":"CR6","unstructured":"Birtwistle, G. and Subrahmanyam, P. A. (eds.): VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers (1988)."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"de Bruijn, N. G.: ?A survey of the project AUTOMATH?, in: Seldin and Hindley [35], pp. 579?606.","DOI":"10.1016\/S0049-237X(08)70203-9"},{"key":"CR8","unstructured":"Constable, R. L., et al.: Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall (1986)."},{"key":"CR9","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"Th. Coquand","year":"1988","unstructured":"Coquand, Th. and Huet, G.: ?The calculus of constructions?, Information and Computation 76, 95?120 (1988).","journal-title":"Information and Computation"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Coquand, Th. and Huet, G., ?Constructions: a higher order proof system for mechanizing mathematics?, in: Buchberger, B., editor, EUROCAL '85: European Conference on Computer Algebra, Volume 1: Invited lectures, Springer (1985), 151?184.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"CR11","unstructured":"Dummett, M.: Elements of Intuitionism, Oxford University Press (1977)."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Felty, A. and Miller, D.: ?Specifying theorem provers in a higher-order logic programming language?, in Ninth Conference on Automated Deduction, Lusk, E. and Overbeek, R. (eds.), Springer (1988), pp. 61?80.","DOI":"10.1007\/BFb0012823"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Gordon, M. J. C., ?HOL: A proof generating system for higher-order logic?, in: Birtwistle and Subrahmanyam [6], pp. 79?128.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"CR14","volume-title":"How I spent my time in Cambridge with Isabelle","author":"Ph. Groote de","year":"1987","unstructured":"de Groote, Ph., ?How I spent my time in Cambridge with Isabelle?, Report RR 87?1, Unit\u00e9 d'informatique, Universit\u00e9 Catholique de Louvain, Belgium (1987)."},{"key":"CR15","unstructured":"Harper, R., Honsell, F., and Plotkin, G.: ?A Framework for Defining Logics?, Proceedings of a symposium on Logic in Computer Science (IEEE, 1987), pp. 194?204."},{"key":"CR16","unstructured":"Hindley, J. R. and Seldin, J. P.: Introduction to Combinators and ?-calculus, Cambridge University Press (1986)."},{"key":"CR17","unstructured":"Hoare, C. A. R. and Shepherdson, J. C. (eds.); Mathematical Logic and Programming Languages, Prentice-Hall (1985)."},{"key":"CR18","unstructured":"Howard, W. A.: ?The formulae-as-types notion of construction?, in: Seldin and Hindley [35], pp. 479?490."},{"key":"CR19","doi-asserted-by":"crossref","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 ?-calculus?, Theoretical Computer Science 1, 27?57 (1975).","journal-title":"Theoretical Computer Science"},{"key":"CR20","first-page":"31","volume":"11","author":"G. P. Huet","year":"1978","unstructured":"Huet, G. P. and Lang, B.: ?Proving and applying program transformations expressed with second-order patterns?, Acta Informatica 11 (1978) 31?55.","journal-title":"Acta Informatica"},{"key":"CR21","unstructured":"Jutting, L. S.: Checking Landau's ?Grundlagen? in the AUTOMATH system, Ph.D. Thesis, Technische Hogeschool, Eindhoven (1977)."},{"key":"CR22","unstructured":"Lambek, J. and Scott, P. J.: Introduction to Higher Order Categorical Logic, Cambridge University Press (1986)."},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: ?Constructive mathematics and computer programming?, in: Hoare and Shepherdson [17], pp. 167?184.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"CR24","unstructured":"Martin-L\u00f6f, P.: ?On the meanings of the logical constants and the justifications of the logical laws,? Report, Department of Mathematics, University of Stockholm (1986)."},{"key":"CR25","unstructured":"Martin-L\u00f6f, P.: ?Amendment to intuitionistic type theory?, Lecture notes obtained from P. Dybjer, Computer Science Department, Chalmers University, Gothenburg (1986)."},{"key":"CR26","unstructured":"Milner, R.: ?The use of machines to assist in rigorous proof?, in: Hoare and Shepherdson [17], pp. 77?88."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/BF02136027","volume":"24","author":"B. Nordstr\u00f6m","year":"1984","unstructured":"Nordstr\u00f6m, B. and Smith, J. M.: ?Propositions and specifications of programs in Martin-L\u00f6f's type theory?, BIT 24 (1984) 288?301.","journal-title":"BIT"},{"key":"CR28","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. C. Paulson","year":"1986","unstructured":"Paulson, L. C.: ?Natural deduction as higher-order resolution?, Journal of Logic Programming 3 (1986) 237?258.","journal-title":"Journal of Logic Programming"},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press (1987).","DOI":"10.1017\/CBO9780511526602"},{"key":"CR30","unstructured":"Paulson, L. C.: ?A preliminary user's manual for Isabelle?, Report 133, Computer Laboratory, University of Cambridge (1988)."},{"key":"CR31","unstructured":"Prawitz, D.: Natural Deduction: A Proof-theoretical Study, Almquist and Wiksell (1965)."},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Prawitz, D.: ?Ideas and results in proof theory?, in: Fenstad, J. E. (ed.): Proceedings of the Second Scandinavian Logic Symposium, North-Holland (1971), pp. 235?308.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"CR33","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P. Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P.: ?A natural extension of natural deduction?, Journal of Symbolic Logic 49 (1984) 1284?1300.","journal-title":"Journal of Symbolic Logic"},{"key":"CR34","unstructured":"Schroeder-Heister, P.: ?Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ?, ?, ?, ?, ??, in: M. M. Richter et al. (eds.): Logic Colloquium '83, Springer Lecture Notes in Mathematics 1104 (1984)."},{"key":"CR35","unstructured":"Seldin, J. P. and Hindley, J. R.: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press (1980)."},{"key":"CR36","unstructured":"Takeuti, G.: Proof Theory (2nd edition), North Holland (1987)."},{"key":"CR37","unstructured":"Whitehead, A. N. and Russell, B.: Principia Mathematica, Paperback edition to ?56, Cambridge University Press (1962)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00248324.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00248324\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00248324","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T15:55:49Z","timestamp":1554306949000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00248324"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,9]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1989,9]]}},"alternative-id":["BF00248324"],"URL":"https:\/\/doi.org\/10.1007\/bf00248324","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,9]]}}}