{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T04:54:12Z","timestamp":1768452852248,"version":"3.49.0"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661063","type":"print"},{"value":"9783319661070","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_15","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"225-240","source":"Crossref","is-referenced-by-count":4,"title":["Formalizing Basic Quaternionic Analysis"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Gabrielli","sequence":"first","affiliation":[]},{"given":"Marco","family":"Maggesi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"15_CR1","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-010-9198-6","volume":"47","author":"G Ciolli","year":"2011","unstructured":"Ciolli, G., Gentili, G., Maggesi, M.: A certified proof of the Cartan fixed point theorems. J. Automated Reason. 47(3), 319\u2013336 (2011). https:\/\/doi.org\/10.1007\/s10817-010-9198-6","journal-title":"J. Automated Reason."},{"issue":"4","key":"15_CR2","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1016\/j.cagd.2007.09.007","volume":"25","author":"RT Farouki","year":"2008","unstructured":"Farouki, R.T., Giannelli, C., Manni, C., Sestini, A.: Identification of spatial PH quintic hermite interpolants with near-optimal shape measures. Comput. Aided Geom. Des. 25(4), 274\u2013297 (2008)","journal-title":"Comput. Aided Geom. Des."},{"key":"15_CR3","series-title":"Geometry and Computing","volume-title":"Pythagorean-Hodograph Curves: Algebra and Geometry Inseparable","author":"R Farouki","year":"2009","unstructured":"Farouki, R.: Pythagorean-Hodograph Curves: Algebra and Geometry Inseparable. Geometry and Computing. Springer, Heidelberg (2009)"},{"issue":"2","key":"15_CR4","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"},{"key":"15_CR5","series-title":"Springer Monographs in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33871-7","volume-title":"Regular Functions of a Quaternionic Variable","author":"G Gentili","year":"2013","unstructured":"Gentili, G., Stoppato, C., Struppa, D.: Regular Functions of a Quaternionic Variable. Springer Monographs in Mathematics. Springer, Heidelberg (2013)"},{"issue":"10","key":"15_CR6","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1016\/j.crma.2006.03.015","volume":"342","author":"G Gentili","year":"2006","unstructured":"Gentili, G., Struppa, D.C.: A new approach to Cullen-regular functions of a quaternionic variable. Comptes Rendus Math. 342(10), 741\u2013744 (2006)","journal-title":"Comptes Rendus Math."},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114\u2013129. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_8"},{"key":"15_CR8","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. 10, no. 23, pp. 151\u2013165. University of Bia\u0142ystok (2007). http:\/\/mizar.org\/trybulec65\/"},{"issue":"4","key":"15_CR9","doi-asserted-by":"publisher","first-page":"1305","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), 1305\u20131330 (2016)","journal-title":"Adv. Appl. Clifford Algebras"},{"key":"15_CR10","volume-title":"Calculus on Manifolds: A Modern Approach to Classical Theorems of Advanced Calculus. Advanced Book Program","author":"M Spivak","year":"1965","unstructured":"Spivak, M.: Calculus on Manifolds: A Modern Approach to Classical Theorems of Advanced Calculus. Advanced Book Program. Avalon Publishing, New York (1965)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Sudbery, A.: Quaternionic analysis. Math. Proc. Cambridge Philos. Soc. 85(02), 199\u2013225 (1979)","DOI":"10.1017\/S0305004100055638"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:06:25Z","timestamp":1664431585000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}