{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:27:31Z","timestamp":1664432851810},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,8,19]],"date-time":"2010-08-19T00:00:00Z","timestamp":1282176000000},"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":[[2011,10]]},"DOI":"10.1007\/s10817-010-9198-6","type":"journal-article","created":{"date-parts":[[2010,8,18]],"date-time":"2010-08-18T05:15:51Z","timestamp":1282108551000},"page":"319-336","source":"Crossref","is-referenced-by-count":1,"title":["A Certified Proof of the Cartan Fixed Point Theorems"],"prefix":"10.1007","volume":"47","author":[{"given":"Gianni","family":"Ciolli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graziano","family":"Gentili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Maggesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,8,19]]},"reference":[{"key":"9198_CR1","volume-title":"An Introduction to the Theory of Analytic Functions of One Complex Variable, International Series in Pure and Applied Mathematics","author":"LV Ahlfors","year":"1978","unstructured":"Ahlfors, L.V.: Complex analysis, 3rd edn. In: An Introduction to the Theory of Analytic Functions of One Complex Variable, International Series in Pure and Applied Mathematics. McGraw-Hill Book Co., New York (1978)","edition":"3"},{"issue":"3","key":"9198_CR2","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1090\/S0894-0347-1994-1242454-2","volume":"7","author":"DM Burns","year":"1994","unstructured":"Burns, D.M., Krantz, S.G.: Rigidity of holomorphic mappings and a new Schwarz lemma at the boundary. J. Am. Math. Soc. 7(3), 661\u2013676 (1994)","journal-title":"J. Am. Math. Soc."},{"key":"9198_CR3","doi-asserted-by":"crossref","first-page":"199","DOI":"10.24033\/bsmf.1165","volume":"58","author":"H Cartan","year":"1930","unstructured":"Cartan, H.: Sur les fonctions de deux variables complexes. Les transformations d\u2019un domaine born\u00e9 D en un domaine int\u00e9rieur \u00e0 D. Bull. Soc. Math. Fr. 58, 199\u2013219 (1930)","journal-title":"Bull. Soc. Math. Fr."},{"issue":"1","key":"9198_CR4","doi-asserted-by":"crossref","first-page":"760","DOI":"10.1007\/BF01186587","volume":"35","author":"H Cartan","year":"1932","unstructured":"Cartan, H.: Sur les fonctions de plusieurs variables complexes. L\u2019it\u00e9ration des transformations int\u00e9rieures d\u2019un domaine born\u00e9. Math. Z. 35(1), 760\u2013773 (1932)","journal-title":"Math. Z."},{"key":"9198_CR5","doi-asserted-by":"crossref","first-page":"1793","DOI":"10.1016\/j.aim.2009.06.015","volume":"222","author":"F Colombo","year":"2009","unstructured":"Colombo, F., Gentili, G., Sabadini, I., Struppa, D.: Extension results for slice regular functions of a quaternionic variable. Adv. Math. 222, 1793\u20131808 (2009)","journal-title":"Adv. Math."},{"key":"9198_CR6","doi-asserted-by":"crossref","unstructured":"Corbineau, P.: A declarative language for the coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES. Lecture Notes in Computer Science, vol. 4941, pp. 69\u201384. Springer (2007)","DOI":"10.1007\/978-3-540-68103-8_5"},{"key":"9198_CR7","volume-title":"Holomorphic Maps And Invariant Distances. Notas de Matem\u00e1tica [Mathematical Notes], vol. 69","author":"T Franzoni","year":"1980","unstructured":"Franzoni, T., Vesentini, E.: Holomorphic Maps And Invariant Distances. Notas de Matem\u00e1tica [Mathematical Notes], vol. 69. North-Holland Publishing Co., Amsterdam (1980)"},{"issue":"1","key":"9198_CR8","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/BF01292723","volume":"7","author":"R Fueter","year":"1934","unstructured":"Fueter, R.: Die funktionentheorie der differentialgleichungen \u0398u\u2009=\u20090 und \u0398\u0398u\u2009=\u20090 mit vier reellen variablen. Comment. Math. Helv. 7(1), 307\u2013330 (1934)","journal-title":"Comment. Math. Helv."},{"key":"9198_CR9","unstructured":"Gentili, G., Stoppato, C.: Power series and analyticity over the quaternions (2009)"},{"key":"9198_CR10","first-page":"165","volume-title":"Hypercomplex Analysis, Trends in Mathematics","author":"G Gentili","year":"2009","unstructured":"Gentili, G., Stoppato, C., Struppa, D., Vlacci, F.: Recent developments for regular functions of a hypercomplex variable. In: Sabadini, I., Shapiro, M., Sommen, F. (eds.) Hypercomplex Analysis, Trends in Mathematics, pp. 165\u2013185. Birkhauser, Basel (2009)"},{"issue":"10","key":"9198_CR11","doi-asserted-by":"crossref","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. C. R. Math. Acad. Sci. Paris 342(10), 741\u2013744 (2006)","journal-title":"C. R. Math. Acad. Sci. Paris"},{"issue":"1","key":"9198_CR12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.aim.2007.05.010","volume":"216","author":"G Gentili","year":"2007","unstructured":"Gentili, G., Struppa, D.C.: A new theory of regular functions of a quaternionic variable. Adv. Math. 216(1), 279\u2013301 (2007)","journal-title":"Adv. Math."},{"issue":"11","key":"9198_CR13","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. Not. Am. Math. Soc. 55(11), 1382\u20131393 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"11","key":"9198_CR14","first-page":"1370","volume":"55","author":"TC Hales","year":"2008","unstructured":"Hales, T.C.: Formal proof. Not. Am. Math. Soc. 55(11), 1370\u20131380 (2008)","journal-title":"Not. Am. Math. Soc."},{"key":"9198_CR15","unstructured":"Harrison, J.: The HOL Light theorem prover. Freely available on the Internet at http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/ . Accessed 9 August 2010"},{"key":"9198_CR16","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. 1166, pp. 265\u2013269. Springer, Verlag (1996)","DOI":"10.1007\/BFb0031814"},{"key":"9198_CR17","first-page":"154","volume-title":"Types for Proofs and Programs: International Workshop TYPES\u201996. Lecture Notes in Computer Science, vol. 1512","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: Proof style. In: Gim\u00e9nex, E., Pausin-Mohring, C. (eds.) Types for Proofs and Programs: International Workshop TYPES\u201996. Lecture Notes in Computer Science, vol. 1512, pp. 154\u2013172. Springer, Verlag, Aussois, France (1996)"},{"key":"9198_CR18","volume-title":"Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005. Lecture Notes in Computer Science, vol. 3603","author":"J Harrison","year":"2005","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. 3603, Springer, Verlag, Oxford, UK (2005)"},{"key":"9198_CR19","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(23), pp. 151\u2013165. University of Bia\u0142ystok (2007)"},{"issue":"11","key":"9198_CR20","first-page":"1395","volume":"55","author":"J Harrison","year":"2008","unstructured":"Harrison, J.: Formal proof\u2014theory and practice. Not. Am. Math. Soc. 55(11), 1395\u20131406 (2008)","journal-title":"Not. Am. Math. Soc."},{"key":"9198_CR21","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF01425490","volume":"3","author":"W Kaup","year":"1967","unstructured":"Kaup, W.: Reelle transformationsgruppen und invariante Metriken auf komplexen R\u00e4umen. Invent. Math 3, 43\u201370 (1967)","journal-title":"Invent. Math"},{"key":"9198_CR22","series-title":"The Wadsworth & Brooks\/Cole Mathematics Series","volume-title":"Function Theory of Several Complex Variables","author":"SG Krantz","year":"1992","unstructured":"Krantz, S.G.: Function Theory of Several Complex Variables, 2nd edn. The Wadsworth & Brooks\/Cole Mathematics Series. Wadsworth & Brooks\/Cole Advanced Books & Software, Pacific Grove, CA (1992)","edition":"2"},{"key":"9198_CR23","doi-asserted-by":"crossref","unstructured":"Rudin, W.: Function Theory in the Unit Ball of $C\\sp{n}$ . Grundlehren der Mathematischen Wissenschaften, vol. 241. Springer, Verlag (1980)","DOI":"10.1007\/978-1-4613-8098-6"},{"issue":"2","key":"9198_CR24","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1017\/S0305004100055638","volume":"85","author":"A Sudbery","year":"1979","unstructured":"Sudbery, A.: Quaternionic analysis. Math. Proc. Camb. Philos. Soc. 85(2), 199\u2013224 (1979)","journal-title":"Math. Proc. Camb. Philos. Soc."},{"key":"9198_CR25","volume-title":"Capitoli scelti della teoria delle funzioni olomorfe. Quaderni dell\u2019Unione Matematica Italiana","author":"E Vesentini","year":"1984","unstructured":"Vesentini, E.: Capitoli scelti della teoria delle funzioni olomorfe. Quaderni dell\u2019Unione Matematica Italiana. Oderisi, Gubbio (1984)"},{"key":"9198_CR26","unstructured":"Wenzel, M.M., Technische Universit\u00e4t M\u00fcnchen.: Isabelle\/isar\u2014a versatile environment for human-readable formal proof documents (2002)"},{"key":"9198_CR27","unstructured":"Wiedijk, F.: The de bruijn factor (2000)"},{"key":"9198_CR28","unstructured":"Wiedijk, F.: Mizar light for hol light. In: Theorem Proving in Higher Order Logics: TPHOLs 2001. LNCS vol. 2152, pp. 378\u2013393 (2001)"},{"issue":"11","key":"9198_CR29","first-page":"1408","volume":"55","author":"F Wiedijk","year":"2008","unstructured":"Wiedijk, F.: Formal proof\u2014getting started. Not. Am. Math. Soc. 55(11), 1408\u20131417 (2008)","journal-title":"Not. Am. Math. Soc."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9198-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9198-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9198-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T01:48:51Z","timestamp":1559440131000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9198-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,8,19]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,10]]}},"alternative-id":["9198"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9198-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,8,19]]}}}