{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,3]],"date-time":"2026-01-03T14:42:27Z","timestamp":1767451347258},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283720"},{"type":"electronic","value":"9783540318200"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_8","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T19:12:52Z","timestamp":1279653172000},"page":"114-129","source":"Crossref","is-referenced-by-count":66,"title":["A HOL Theory of Euclidean Space"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Blume, M.: No-longer-foreign: Teaching an ML compiler to speak C \u201cnatively\u201d. In: Benton, N., Kennedy, A. (eds.) BABEL 2001: First workshop on multi-language infrastructure and interoperability (2001), Available online via http:\/\/docs.msdnaa.net\/ark_new\/Webfiles\/babel.htm","key":"8_CR1","DOI":"10.1016\/S1571-0661(05)80452-9"},{"key":"8_CR2","series-title":"Ergebnisse der Mathematik und ihrer Grenzgebiete","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03718-8","volume-title":"Real Algebraic Geometry","author":"J. Bochnak","year":"1998","unstructured":"Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. Ergebnisse der Mathematik und ihrer Grenzgebiete, vol.\u00a036. Springer, Heidelberg (1998)"},{"key":"8_CR3","first-page":"1133","volume":"38","author":"W.M. Farmer","year":"1991","unstructured":"Farmer, W.M., Thayer, F.J.: Two computer-supported proofs in metric space topology. Notices of the American Mathematical Society\u00a038, 1133\u20131138 (1991)","journal-title":"Notices of the American Mathematical Society"},{"doi-asserted-by":"crossref","unstructured":"G\u00e5rding, L.: Some Points of Analysis and Their History. University Lecture Series, vol.\u00a011. American Mathematical Society \/ Higher Education Press (1997)","key":"8_CR4","DOI":"10.1090\/ulect\/011"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45842-5_7","volume-title":"Types for Proofs and Programs","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A constructive proof of the fundamental theorem of algebra without using the rationals. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 96\u2013111. Springer, Heidelberg (2002)"},{"key":"8_CR6","series-title":"IFIP Transactions A: Computer Science and Technology","first-page":"145","volume-title":"Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"J. Harrison","year":"1992","unstructured":"Harrison, J.: Constructing the real numbers in HOL. In: Claesen, L.J.M., Gordon, M.J.C. (eds.) Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium. IFIP Transactions A: Computer Science and Technology, vol.\u00a0A-20, pp. 145\u2013164. North-Holland, Amsterdam (1992)"},{"unstructured":"Harrison, J.: Complex quantifier elimination in HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001: Supplemental Proceedings, Division of Informatics, University of Edinburgh, Published as Informatics Report Series EDI-INF-RR-0046, pp. 159\u2013174 (2001), Available on the Web, at http:\/\/www.informatics.ed.ac.uk\/publications\/report\/0046.html","key":"8_CR7"},{"key":"8_CR8","volume-title":"Grundlehren der mathematischen Wissenschaften","author":"L. H\u00f6rmander","year":"1983","unstructured":"H\u00f6rmander, L.: The Analysis of Linear Partial Differential Operators II. In: Grundlehren der mathematischen Wissenschaften, vol.\u00a0257. Springer, Heidelberg (1983)"},{"unstructured":"Jutting, L.S.v.B.: CHecking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, Useful summary in [13], pp. 701\u2013732 (1977)","key":"8_CR9"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1147\/rd.45.0518","volume":"4","author":"H.W. Kuhn","year":"1960","unstructured":"Kuhn, H.W.: Some combinatorial lemmas in topology. IBM Journal of research and development\u00a04, 518\u2013524 (1960), Available on the Web from http:\/\/www.research.ibm.com\/journal\/rd\/045\/ibmrd0405K.pdf","journal-title":"IBM Journal of research and development"},{"doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: To appear in proceedings of the 20th International Conference on Automated Deduction (2005)","key":"8_CR11","DOI":"10.1007\/11532231_22"},{"unstructured":"Milewski, R.: Fundamental theorem of algebra. Journal of Formalized Mathematics, 12 (2000), See http:\/\/mizar.org\/JFM\/Vol12\/polynom5.html","key":"8_CR12"},{"key":"8_CR13","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Selected Papers on Automath","year":"1994","unstructured":"Nederpelt, R.P., Geuvers, J.H., Vrijer, R.C.d. (eds.): Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol.\u00a0133. North-Holland, Amsterdam (1994)"},{"unstructured":"Parrilo, P.: Semidefinite programming relaxations for semialgebraic problems (2001), Available from the Web at citeseer.nj.nec.com\/parrilo01semidefinite.html","key":"8_CR14"},{"key":"8_CR15","volume-title":"Principles of Mathematical Analysis","author":"W. Rudin","year":"1976","unstructured":"Rudin, W.: Principles of Mathematical Analysis, 3rd edn. McGraw-Hill, New York (1976)","edition":"3"},{"unstructured":"Solovay, R.: Elimination of quantifiers I, II, III. Email messages to John Harrison, 9, 19, 20 and 27 November 2004 (2004)","key":"8_CR16"},{"key":"8_CR17","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/978-1-4757-6095-8_20","volume-title":"Optimal control: theory, algorithms, and applications","author":"H.J. Sussmann","year":"1998","unstructured":"Sussmann, H.J.: Multidifferential calculus: chain rule, open mapping and transversal intersection theorems. In: Hager, W.W., Pardalos, P.M. (eds.) Optimal control: theory, algorithms, and applications, pp. 436\u2013487. Kluwer, Dordrecht (1998)"}],"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\/11541868_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T22:49:40Z","timestamp":1635720580000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11541868_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}