{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:21:07Z","timestamp":1764350467591,"version":"3.37.3"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T00:00:00Z","timestamp":1543881600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"National Key R & D Program","award":["2017YFC0806700"],"award-info":[{"award-number":["2017YFC0806700"]}]},{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61876111","61472468"],"award-info":[{"award-number":["61876111","61472468"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61572331"],"award-info":[{"award-number":["61572331"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Capacity Building for Sci-Tech Innovation \u2013 Fundamental Scientific Research Funds","award":["025185305000"],"award-info":[{"award-number":["025185305000"]}]},{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61602325"],"award-info":[{"award-number":["61602325"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.1007\/s10817-018-9498-9","type":"journal-article","created":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T03:52:37Z","timestamp":1543895557000},"page":"787-808","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalization of Geometric Algebra in HOL Light"],"prefix":"10.1007","volume":"63","author":[{"given":"Li-Ming","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3562-8602","authenticated-orcid":false,"given":"Zhi-Ping","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qian-Ying","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong-Dong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,12,4]]},"reference":[{"key":"9498_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-4728-3_1","volume-title":"A Unified Language for Mathematics and Physics","author":"D Hestenes","year":"1986","unstructured":"Hestenes, D.: A Unified Language for Mathematics and Physics. Springer, Netherlands (1986)"},{"issue":"1","key":"9498_CR2","doi-asserted-by":"publisher","first-page":"63","DOI":"10.4173\/mic.2016.1.6","volume":"37","author":"AL Kleppe","year":"2016","unstructured":"Kleppe, A.L., Egeland, O.: Inverse kinematics for industrial robots using conformal geometric algebra. Model. Identif. Control 37(1), 63\u201375 (2016)","journal-title":"Model. Identif. Control"},{"issue":"5","key":"9498_CR3","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1002\/rob.21572","volume":"32","author":"MJ Stanway","year":"2015","unstructured":"Stanway, M.J., Kinsey, J.C.: Rotation identification in geometric algebra: theory and application to the navigation of underwater robots in the field. J. Field Robot. 32(5), 632\u2013654 (2015)","journal-title":"J. Field Robot."},{"issue":"16","key":"9498_CR4","doi-asserted-by":"publisher","first-page":"2213","DOI":"10.1016\/j.patrec.2011.05.014","volume":"32","author":"M Bernal-Marin","year":"2011","unstructured":"Bernal-Marin, M., Bayro-Corrochano, E.: Integration of Hough transform of lines and planes in the framework of conformal geometric algebra for 2D and 3D robot vision. Pattern Recognit. Lett. 32(16), 2213\u20132223 (2011)","journal-title":"Pattern Recognit. Lett."},{"issue":"3","key":"9498_CR5","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1016\/j.vlsi.2008.09.010","volume":"42","author":"S Franchini","year":"2009","unstructured":"Franchini, S., Gentile, A., Sorbello, F., Vassallo, G., Vitabile, S.: An embedded, FPGA-based computer graphics coprocessor with native geometric algebra support. Integr. VlSI J. 42(3), 346\u2013355 (2009)","journal-title":"Integr. VlSI J."},{"issue":"5","key":"9498_CR6","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1119\/1.14223","volume":"53","author":"D Hestenes","year":"1985","unstructured":"Hestenes, D., Sobczyk, G., Marsh, J.S.: Clifford algebra to geometric calculus: a unified language formathematics and physics. Am. J. Phys. 53(5), 510\u2013511 (1985)","journal-title":"Am. J. Phys."},{"key":"9498_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0089-5","volume-title":"Applications of Geometric Algebra in Computer Science and Engineering","author":"L Dorst","year":"2002","unstructured":"Dorst, L., Doran, C., Lasenby, J.: Applications of Geometric Algebra in Computer Science and Engineering. Birkhauser, Basel (2002)"},{"issue":"1","key":"9498_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF03161249","volume":"27","author":"A Macdonald","year":"2016","unstructured":"Macdonald, A.: A survey of geometric algebra and geometric calculus. Adv. Appl. Clifford Algebras 27(1), 1\u201339 (2016)","journal-title":"Adv. Appl. Clifford Algebras"},{"issue":"2","key":"9498_CR9","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.cpc.2005.04.001","volume":"170","author":"R Ab\u0142amowicz","year":"2002","unstructured":"Ab\u0142amowicz, R., Fauser, B.: Clifford and Gra\u00dfmann Hopf algebras via the BIGEBRA package for Maple. Comput. Phys. Commun. 170(2), 115\u2013130 (2002)","journal-title":"Comput. Phys. Commun."},{"key":"9498_CR10","unstructured":"Aragoncamarasa, G., Aragongonzalez, G., Aragon, J.L., Rodriguezandrade, M.A.: Clifford algebra with mathematica. Physics (2008). Preprint. \n                    arXiv:0810.2412\n                    \n                  . October 2008"},{"key":"9498_CR11","volume-title":"The Making of GABLE: A Geometric Algebra Learning Environment in Matlab","author":"S Mann","year":"2001","unstructured":"Mann, S., Dorst, L., Bouma, T.: The Making of GABLE: A Geometric Algebra Learning Environment in Matlab. Birkh\u00fcser, Boston (2001)"},{"issue":"2","key":"9498_CR12","first-page":"317","volume":"89","author":"MJC Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. FEBS Lett. 89(2), 317\u2013320 (1993)","journal-title":"FEBS Lett."},{"key":"9498_CR13","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). Volume 1166 of Lecture Notes in Computer Science., Springer, pp. 265\u2013269 (1996)","DOI":"10.1007\/BFb0031814"},{"key":"9498_CR14","volume-title":"Isabelle\u2014A Generic Theorem Prover","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle\u2014A Generic Theorem Prover. LNCS, Heidelberg (1994)"},{"key":"9498_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Berlin (2004)"},{"key":"9498_CR16","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/BFb0105402","volume":"1125","author":"B Dutertre","year":"1999","unstructured":"Dutertre, B.: Elements of mathematical analysis in PVS. Lect. Notes Comput. Sci. 1125, 141\u2013156 (1999)","journal-title":"Lect. Notes Comput. Sci."},{"key":"9498_CR17","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S., Kaufmann, M., Moore, J.S.: Acl2 Computer Aided Reasoning: An Approach (vol 1). World Scientific Publishing Company 81(957), 1\u201327 (2002)"},{"issue":"3","key":"9498_CR18","first-page":"311","volume":"31","author":"P Rudnicki","year":"1994","unstructured":"Rudnicki, P.: An overview of the Mizar project. Univ. Technol. Bastad 31(3), 311\u2013332 (1994)","journal-title":"Univ. Technol. Bastad"},{"key":"9498_CR19","unstructured":"Arthan, R.: Mathematical Case Studies: The Geometric Algebra (2006). \n                    http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.696.1120.\n                    \n                   May 2012"},{"issue":"2","key":"9498_CR20","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s00006-014-0447-3","volume":"24","author":"L Fuchs","year":"2014","unstructured":"Fuchs, L., Th\u00e9ry, L.: Implementing geometric algebra products with binary trees. Adv. Appl. Clifford Algebras 24(2), 589\u2013611 (2014)","journal-title":"Adv. Appl. Clifford Algebras"},{"issue":"2","key":"9498_CR21","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL Light theory of Euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9498_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00006-016-0650-5","volume":"26","author":"S Ma","year":"2016","unstructured":"Ma, S., Shi, Z., Shao, Z., Guan, Y., Li, L., Li, Y.: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. Adv. Appl. Clifford Algebras 26(4), 1\u201326 (2016)","journal-title":"Adv. Appl. Clifford Algebras"},{"key":"9498_CR23","unstructured":"Harrison, J.: The HOL Light theorem prover. \n                    http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/\n                    \n                  . Accessed 6 Aug 2016"},{"key":"9498_CR24","unstructured":"Harrison, J.: HOL Light: an overview. 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. Volume 5674 of Lecture Notes in Computer Science., Munich, Germany, Springer-Verlag 60\u201366 (2009)"},{"issue":"3","key":"9498_CR25","first-page":"47","volume":"16","author":"T Hales","year":"2015","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T.: A formal proof of the Kepler conjecture. Mathematics 16(3), 47\u201358 (2015)","journal-title":"Mathematics"},{"key":"9498_CR26","unstructured":"Harrison, J.: Geometric algebra. \n                    https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/Multivariate\/clifford.ml\n                    \n                  . Accessed 4 May 2016"},{"key":"9498_CR27","doi-asserted-by":"crossref","unstructured":"Rivera-Rovelo, J., Bayro-Corrochano, E.: Medical image segmentation using a self-organizing neural network and Clifford geometric algebra. In: International Joint Conference on Neural Networks, pp. 3538\u20133545 (2006)","DOI":"10.1109\/IJCNN.2006.247362"},{"key":"9498_CR28","doi-asserted-by":"crossref","unstructured":"Hestenes, D., Li, H., Rockwood, A.: New algebraic tools for classical geometry. Geometric Computing with Clifford Algebras, pp. 3\u201326 (2001)","DOI":"10.1007\/978-3-662-04621-0_1"},{"issue":"458","key":"9498_CR29","first-page":"703","volume":"71","author":"D Hestenes","year":"2002","unstructured":"Hestenes, D.: New foundations for classical mechanics. Math. Gaz. 71(458), 703\u2013704 (2002)","journal-title":"Math. Gaz."},{"key":"9498_CR30","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. Volume 3603 of Lecture Notes in Computer Science., Oxford, UK, Springer-Verlag, pp. 114\u2013129 (2005)","DOI":"10.1007\/11541868_8"},{"key":"9498_CR31","unstructured":"Harrison, J.: Definition of finite Cartesian product types. \n                    https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/cart.ml\n                    \n                  . Accessed 16 May 2016"},{"key":"9498_CR32","unstructured":"Harrison, J.: Real vectors in Euclidean space, and elementary linear algebra. \n                    https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/Multivariate\/vectors.ml\n                    \n                  . Accessed 11 June 2016"},{"key":"9498_CR33","unstructured":"Harrison, J.: Determinant and trace of a square matrix. \n                    https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/Multivariate\/determinants.ml\n                    \n                  . Accessed 11 Jan 2016"},{"key":"9498_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0089-5_2","volume-title":"The Inner Products of Geometric Algebra","author":"L Dorst","year":"2002","unstructured":"Dorst, L.: The Inner Products of Geometric Algebra. Birkh\u00e4user, Boston (2002)"},{"issue":"2","key":"9498_CR35","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1006\/jsco.1995.1046","volume":"20","author":"D Hartley","year":"1995","unstructured":"Hartley, D., Tuckey, P.: Gr\u00f6bner bases in Clifford and Grassmann algebras. J. Symb. Comput. 20(2), 197\u2013205 (1995)","journal-title":"J. Symb. Comput."},{"key":"9498_CR36","unstructured":"Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Volume 10(23) of Studies in Logic, Grammar and Rhetoric, pp. 151\u2013165. University of Bia\u0142ystok (2007)"},{"key":"9498_CR37","doi-asserted-by":"crossref","unstructured":"Gabrielli, A., Maggesi, M.: In: Formalizing Basic Quaternionic Analysis. Springer, Cham pp. 225\u2013240 (2017)","DOI":"10.1007\/978-3-319-66107-0_15"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9498-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9498-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9498-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,3]],"date-time":"2019-12-03T19:10:04Z","timestamp":1575400204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9498-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,4]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["9498"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9498-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,12,4]]},"assertion":[{"value":"23 November 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 December 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}