{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:47:15Z","timestamp":1777578435552,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540649878","type":"print"},{"value":"9783540498018","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055135","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"153-170","source":"Crossref","is-referenced-by-count":20,"title":["Formalizing basic first order model theory"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. Bruijn de","year":"1972","unstructured":"N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34, 381\u2013392, 1972.","journal-title":"Indagationes Mathematicae"},{"key":"10_CR2","unstructured":"H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972."},{"key":"10_CR3","first-page":"173","volume-title":"Volume 1125 of Lecture Notes in Computer Science","author":"A. D. Gordon","year":"1996","unstructured":"A. D. Gordon and T. Melham. Five axioms of alpha-conversion. In J. von Wright, J. Grundy, and J. Harrison (eds.), Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Volume 1125 of Lecture Notes in Computer Science, Turku, Finland, pp. 173\u2013190. Springer-Verlag, 1996."},{"key":"10_CR4","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"P. T. Johnstone. Notes on Logic and Set Theory. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9781139172066"},{"key":"10_CR6","unstructured":"G. Kreisel and J.-L. Krivine. Elements of mathematical logic: model theory (Revised second ed.). Studies in Logic and the Foundations of Mathematics. North-Holland, 1971. First edition 1967. Translation of the French \u2018El\u00e9ments de logique math\u00e9matique, th\u00e9orie des modeles\u2019 published by Dunod, Paris in 1964."},{"key":"10_CR7","first-page":"3","volume-title":"Volume A-20 of IFIP Transactions A: Computer Science and Technology","author":"T. F. Melham","year":"1992","unstructured":"T. F. Melham. The HOL logic extended with quantification over type variables. In L. J. M. Claesen. and M. J. C. Gordon. (eds.), Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, Volume A-20 of IFIP Transactions A: Computer Science and Technology, IMEC, Leuven, Belgium, pp. 3\u201318. North-Holland, 1992."},{"key":"10_CR8","volume-title":"Licentiate thesis","author":"H. Persson","year":"1996","unstructured":"H. Persson. Constructive Completeness of Intuitionistic Predicate Logic: A Formalisation in Type Theory. Licentiate thesis, Department of Computing Science, Chalmers University of Technology and University of G\u00f6teborg, Sweden, 1996."},{"key":"10_CR9","unstructured":"R. Pollack. The theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. Ph. D. thesis, University of Edinburgh, 1994."},{"key":"10_CR10","unstructured":"D. Prawitz. Natural deduction; a proof-theoretical study, Volume 3 of Stockholm Studies in Philosophy. Almqvist and Wiksells, 1965."},{"key":"10_CR11","unstructured":"P. Rudnicki. An overview of the MIZAR project, 1992. Available by anonymous FTP from menaik.cs.ualberta.ca as pub\/Mizar\/Mizar_Over.tar.Z."},{"key":"10_CR12","unstructured":"S. Shapiro. Foundations without Foundationalism: A case for second-order logic. Number 17 in Oxford Logic Guides. Clarendon Press, 1991."},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90149-1","volume":"17","author":"A. Stoughton","year":"1988","unstructured":"A. Stoughton. Substitution revisited. Theoretical Computer Science, 17, 317\u2013325, 1988.","journal-title":"Theoretical Computer Science"},{"key":"10_CR14","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"A. Trybulec. The Mizar-QC\/6000 logic information language. ALLC Bulletin (Association for Literary and Linguistic Computing), 6, 136\u2013140, 1978.","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T11:56:35Z","timestamp":1549886195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0055135","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}