{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:15Z","timestamp":1762458975027,"version":"3.40.3"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,4,19]],"date-time":"2012-04-19T00:00:00Z","timestamp":1334793600000},"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":[[2013,2]]},"DOI":"10.1007\/s10817-012-9250-9","type":"journal-article","created":{"date-parts":[[2012,4,18]],"date-time":"2012-04-18T00:41:10Z","timestamp":1334709670000},"page":"173-190","source":"Crossref","is-referenced-by-count":76,"title":["The HOL Light Theory of Euclidean Space"],"prefix":"10.1007","volume":"50","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,4,19]]},"reference":[{"key":"9250_CR1","unstructured":"Fontaine, P.: Techniques for verification of concurrent systems with invariants. Ph.D. thesis, Institut Montefiore, Universit\u00e9 de Li\u00e8ge (2004)"},{"key":"9250_CR2","doi-asserted-by":"crossref","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 for Proofs and Programs, Proceedings of the International Workshop, TYPES 2000. Lecture Notes in Computer Science, vol.\u00a02277, pp.\u00a096\u2013111. Springer (2001)","DOI":"10.1007\/3-540-45842-5_7"},{"key":"9250_CR3","unstructured":"Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol.\u00a005021. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2006)"},{"key":"9250_CR4","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1080\/00029890.2007.11920481","volume":"114","author":"TC Hales","year":"2007","unstructured":"Hales, T.C.: The Jordan curve theorem, formally and informally. Am. Math. Mon. 114, 882\u2013894 (2007)","journal-title":"Am. Math. Mon."},{"key":"9250_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00454-009-9148-4","volume":"44","author":"TC Hales","year":"2010","unstructured":"Hales, T.C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., Zumkeller, R.: A revision of the proof of the Kepler conjecture. Discrete Comput. Geom. 44, 1\u201334 (2010)","journal-title":"Discrete Comput. Geom."},{"key":"9250_CR6","doi-asserted-by":"crossref","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201996), Lecture Notes in Computer Science, vol.\u00a01166, pp.\u00a0265\u2013269. Springer (1996)","DOI":"10.1007\/BFb0031814"},{"key":"9250_CR7","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer (1998). Revised version of author\u2019s Ph.D. thesis"},{"key":"9250_CR8","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005. Lecture Notes in Computer Science, vol.\u00a03603, pp. 114\u2013129. Springer, Oxford, UK (2005)","DOI":"10.1007\/11541868_8"},{"key":"9250_CR9","unstructured":"Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol.\u00a010(23), pp.\u00a0151\u2013165. University of Bia\u0142ystok (2007)"},{"key":"9250_CR10","unstructured":"Harrison, J.: Without loss of generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009. Lecture Notes in Computer Science, vol.\u00a05674, pp. 43\u201359. Springer, Munich, Germany (2009)"},{"key":"9250_CR11","doi-asserted-by":"crossref","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999. Lecture Notes in Computer Science, vol.\u00a01690, pp. 311\u2013321. Springer, Nice, France (1999)","DOI":"10.1007\/3-540-48256-3_21"},{"key":"9250_CR12","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2001)"},{"key":"9250_CR13","unstructured":"Jutting, L.S.v.B.: Checking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH system. Ph.D. thesis, Eindhoven University of Technology (1977). Useful summary in 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, pp. 701\u2013732. North-Holland (1994)"},{"key":"9250_CR14","doi-asserted-by":"crossref","unstructured":"Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) First International Conference on Interactive Theorem Proving, ITP 2010. Lecture Notes in Computer Science, vol.\u00a06172, pp.\u00a0307\u2013322. Springer, Edinburgh, UK (2010)","DOI":"10.1007\/978-3-642-14052-5_22"},{"key":"9250_CR15","doi-asserted-by":"crossref","first-page":"518","DOI":"10.1147\/rd.45.0518","volume":"4","author":"HW Kuhn","year":"1960","unstructured":"Kuhn, H.W.: Some combinatorial lemmas in topology. IBM J. Res. Dev. 4, 518\u2013524 (1960)","journal-title":"IBM J. Res. Dev."},{"key":"9250_CR16","unstructured":"Milewski, R.: Fundamental theorem of algebra. J. Formal. Math. 12 (2000). http:\/\/mizar.org\/JFM\/Vol12\/polynom5.html"},{"key":"9250_CR17","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 1\u201311 (2010)","DOI":"10.29007\/36dt"},{"key":"9250_CR18","unstructured":"Solovay, R.M., Arthan, R., Harrison, J.: Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904.3482. Submitted to Ann. Pure Appl. Logic. Available at http:\/\/arxiv.org\/abs\/0904.3482 (2009)"},{"key":"9250_CR19","doi-asserted-by":"crossref","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 (1998)","DOI":"10.1007\/978-1-4757-6095-8_20"},{"key":"9250_CR20","doi-asserted-by":"crossref","unstructured":"Webster, R.: Convexity. Oxford University Press (1995)","DOI":"10.1093\/oso\/9780198531470.001.0001"},{"key":"9250_CR21","unstructured":"Wiedijk, F.: Statistics on digital libraries of mathematics. In: Grabowski, A., Naumowicz, A. (eds.) Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric, vol.\u00a018(31). University of Bia\u0142ystok (2009)"},{"key":"9250_CR22","unstructured":"Yee, L.-P., V\u00fdborn\u00fd, R.: The Integral: An Easy Approach After Kurzweil and Henstock. Australian Mathematical Society Lecture Series. Cambridge University Press (2000)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9250-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9250-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9250-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:21:25Z","timestamp":1742944885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9250-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,19]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["9250"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9250-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2012,4,19]]}}}