{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:48:46Z","timestamp":1776552526208,"version":"3.51.2"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"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":[[1993]]},"DOI":"10.1007\/bf00881906","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:37:28Z","timestamp":1104133048000},"page":"213-248","source":"Crossref","is-referenced-by-count":89,"title":["IMPS: An interactive mathematical proof system"],"prefix":"10.1007","volume":"11","author":[{"given":"William M.","family":"Farmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua D.","family":"Guttman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F. Javier","family":"Thayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"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., Issar, S., Nesmith, D. and Pfennig, F., ?The TPS theorem proving system (system abstract)?, in M. E. Stickel (ed.),10th International Conference on Automated Deduction, Vol. 449 ofLecture Notes in Computer Science, pp. 641?642. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_120"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W., ?Some automatic proofs in analysis?, inAutomated Theorem Proving: After 25 Years, pp. 89?118'. American Mathematical Society, 1984.","DOI":"10.1090\/conm\/029\/06"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"509","DOI":"10.2307\/2025179","volume":"72","author":"G. S. Boolos","year":"1975","unstructured":"Boolos, G. S., ?On second-order logic?,J. Philosophy 72 509?527 (1975).","journal-title":"J. Philosophy"},{"key":"CR5","unstructured":"Boyer, R. S. and Moore, J. Strother, ?Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic?, Technical Report ICSCA-CMP-44, Institute for Computing Science, University of Texas at Austin, January 1985."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"Cardelli, L. and Wegner, P., ?On understanding types, data abstraction, and polymorphism?,Computing Surveys 17 471?522 (1985).","journal-title":"Computing Surveys"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A., ?A formulation of the simple theory of types?,J. Symbolic Logic 5 56?68 (1940).","journal-title":"J. Symbolic Logic"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E. and Zhao, X., ?Analytica ? a theorem prover in mathematica?, In D. Kapur (ed.),Automated Deduction ? CADE-11, Vol. 607 ofLecture Notes in Computer Science, pp. 761?765. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_220"},{"key":"CR9","unstructured":"Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T. and Smith, S. F.,Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986."},{"key":"CR10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T. and Huet, G., ?The calculus of constructions?,Information and Computation 76 95?120 (1988).","journal-title":"Information and Computation"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Craigen, D., Kromodimoeljo, S., Meisels, I., Pase, B. and Saaltink, M., ?EVES: an overview?, Technical Report CP-91-5402-43, ORA Corporation, 1991.","DOI":"10.1007\/3-540-54834-3_24"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Craigen, D., Kromodimoeljo, S., Meisels, I., Pase, B. and Saaltink, M., ?EVES system description?, in D. Kapur (Ed.),Automated Deduction ? CADE-11, Vol. 607 ofLecture Notes in Computer Science, pp. 771?775, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_222"},{"key":"CR13","unstructured":"Dieudonn\u00e9, J.,Foundations of Modern Analysis, Academic Press, 1960."},{"key":"CR14","unstructured":"Enderton, H. B.,A Mathematical Introduction to Logic, Academic Press, 1972."},{"key":"CR15","unstructured":"Farmer, W. M., ?Abstract data types in many-sorted second-order logic?, Technical Report M87-64, The MITRE Corporation, 1987."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"1269","DOI":"10.2307\/2274487","volume":"55","author":"W. M. Farmer","year":"1990","unstructured":"Farmer, W. M., ?A partial functions version of Church's simple theory of types?,J. Symbolic Logic 55 1269?91 (1990).","journal-title":"J. Symbolic Logic"},{"key":"CR17","unstructured":"Farmer, W. M., ?A simple type theory with partial functions and sub-types?, Technical report, The MITRE Corporation, 1991."},{"key":"CR18","unstructured":"Farmer, W. M., ?A technique for safely extending axiomatic theories?, Technical report, The MITRE Corporation, 1993."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Farmer, W. M., Guttman, J. D. and Thayer, F. J., ?Little theories?, in D. Kapur (Ed.),Automated Deduction ? CADE-11, Vol. 607 ofLecture Notes in Computer Science, pp. 567?581, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_192"},{"key":"CR20","first-page":"1133","volume":"38","author":"W. M. Farmer","year":"1991","unstructured":"Farmer, W. M. and Thayer, F. J., ?Two computer-supported proofs in metric space topology?,Notices Am. Math. Soc. 38 1133?1138 (1991).","journal-title":"Notices Am. Math. Soc."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2269764","volume":"29","author":"S. Feferman","year":"1964","unstructured":"Feferman, S., ?Systems of predicative analysis?,J. Symbolic Logic,29 1?30 (1964).","journal-title":"J. Symbolic Logic"},{"key":"CR22","unstructured":"Gentzen, G., ?Investigations into logical deduction? (1935), inThe Collected Works of Gerhard Gentzen, North Holland, 1969."},{"key":"CR23","unstructured":"Goguen, J. A., ?Principles of parameterized programming?, Technical report, SRI International, 1987."},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"Goguen, J. A. and Burstall, R. M., ?Introducing institutions?, inLogic of Programs, Vol. 164 ofLecture Notes in Computer Science, pp. 221?256. Springer-Verlag, 1984.","DOI":"10.1007\/3-540-12896-4_366"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Gordon, M., ?HOL: A proof-generating system for higher-order logic?, inVLSI Specification, Verification and Synthesis, Kluwer, 1987.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R. and Wadsworth, C. P.,Edinburgh LCF: A Mechanised Logic of Computation, Vol. 78 ofLecture Notes in Computer Science, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"Grundy, J., ?Window inference in the HOL system?, inProceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pp. 177?89. IEEE Computer Society Press, 1991.","DOI":"10.1109\/HOL.1991.596285"},{"key":"CR28","unstructured":"Guttman, J. D., ?A proposed interface logic for verification environments?, Technical Report M91-19, The MITRE Corporation, 1991."},{"key":"CR29","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Henkin, L., ?Completeness in the theory of types?,J. Symbolic Logic,15 81?91 (1950).","journal-title":"J. Symbolic Logic"},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"Hines, L. M., ?The central variable strategy of strive?, in D. Kapur (ed.),Automated Deduction ? CADE-11, Vol. 607 ofLecture Notes in Computer Science, pp. 35?49, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_154"},{"key":"CR31","unstructured":"Howard, W. A., ?The formulae-as-types notion of construction?, inTo H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479?490, Academic Press, 1980."},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Kohlhase, M., ?Unification in order-sorted type theory?, in A. Voronkov (ed.),Logic Programming and Automated Reasoning, Vol. 624 ofLecture Notes in Computer Science, pp. 421?432, Springer-Verlag, July 1992.","DOI":"10.1007\/BFb0013080"},{"key":"CR33","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1145\/12276.13333","volume":"21","author":"D. Kranz","year":"1986","unstructured":"Kranz, D., Kelsey, R., Rees, J., Hudak, P., Philbin, J. and Adams, N., ?ORBIT: An optimizing compiler for scheme?, inProceedings of the SIGPLAN '86 Symposium on Compiler Construction, Vol. 21, pp. 219?233, 1986.","journal-title":"Proceedings of the SIGPLAN '86 Symposium on Compiler Construction"},{"key":"CR34","first-page":"153","volume-title":"Logic, Methodology, and Philosophy of Science VI","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, P., ?Constructive mathematics and computer programming?, in L. J. Cohen, J. Los, H. Pfeiffer, and K. P. Podewski (ed.),Logic, Methodology, and Philosophy of Science VI, pp. 153?175, Amsterdam, 1982, North-Holland."},{"key":"CR35","doi-asserted-by":"crossref","unstructured":"Monk, J. D.,Mathematical Logic, Springer-Verlag, 1976.","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"CR36","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/BF00297249","volume":"4","author":"L. G. Monk","year":"1988","unstructured":"Monk, L. G., ?Inference rules using local contexts?,J. Automated Reasoning,4 445?462 (1988).","journal-title":"J. Automated Reasoning"},{"key":"CR37","unstructured":"Moschovakis, Y. N.,Elementary Induction on Abstract Structures, North-Holland, 1974."},{"key":"CR38","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BFb0099491","volume":"4","author":"Y. N. Moschovakis","year":"1984","unstructured":"Moschovakis, Y. N., ?Abstract recursion as a foundation for the theory of algorithms?, inComputation and Proof Theory, Vol. 4, pp. 289?364, Springer-Verlag, 1984.","journal-title":"Computation and Proof Theory"},{"key":"CR39","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J. M. and Shankar, N., ?PVS: a prototype verification system?, in D. Kapur (ed.),Automated Deduction ? CADE-11, Vol. 607 ofLecture Notes in Computer Science, pp. 748?752, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"CR40","doi-asserted-by":"crossref","unstructured":"Pase, B. and Kromodimoeljo, S., ?m-Never system summary?, in E. Lusk and R. Overbeek (ed.),9th International Conference on Automated Deduction, Vol. 310Lecture Notes in Computer Science, pp. 738?739, Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012874"},{"key":"CR41","unstructured":"Rees, J. A., Adams, N. I. and Meehan, J. R.,The T Manual, 5th edn, Computer Science Department, Yale University, 1988."},{"key":"CR42","unstructured":"Rushby, J., von Henke, F. and Owre, S., ?An introduction to formal specification and verification using EHDM?, Technical Report SRI-CSL-91-02, SRI International, 1991."},{"key":"CR43","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1093\/mind\/XIV.4.479","volume":"14","author":"B. Russell","year":"1905","unstructured":"Russell, B., ?On denoting?,Mind (New Series),14 479?493 (1905).","journal-title":"Mind"},{"key":"CR44","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"B. Russell","year":"1908","unstructured":"Russell, B., ?Mathematical logic as based on the theory of types?,Am. J. Mathematics,30 222?262 (1908).","journal-title":"Am. J. Mathematics"},{"key":"CR45","doi-asserted-by":"crossref","first-page":"660","DOI":"10.2307\/2274326","volume":"50","author":"S. Shapiro","year":"1985","unstructured":"Shapiro, S., ?Second-order languages and mathematical practice?,J. Symbolic Logic,50 660?696 (1985).","journal-title":"J. Symbolic Logic"},{"key":"CR46","unstructured":"Shoenfield, J. R.,Mathematical Logic, Addison-Wesley, 1967."},{"key":"CR47","unstructured":"Stallman, R. M., GNUEmacs Manual (Version 18), 6th edn, Free Software Foundation, 1987."},{"key":"CR48","unstructured":"Thayer, F. J., ?Obligated term replacements?, Technical Report MTR-10301, The MITRE Corporation, 1987."},{"key":"CR49","doi-asserted-by":"crossref","unstructured":"Weyl, H.,Das Kontinuum, Veit, Leipzig, 1918.","DOI":"10.1515\/9783112451144"},{"key":"CR50","unstructured":"Whitehead, A. N. and Russell, B.,Principia Mathematica, Cambridge University Press, 1910. Paper-back version to Section 56, published 1964."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881906.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881906\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881906","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,21]],"date-time":"2024-12-21T19:05:28Z","timestamp":1734807928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881906"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881906"],"URL":"https:\/\/doi.org\/10.1007\/bf00881906","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}