{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T05:06:07Z","timestamp":1781759167914,"version":"3.54.5"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s11786-016-0254-4","type":"journal-article","created":{"date-parts":[[2016,3,23]],"date-time":"2016-03-23T10:21:10Z","timestamp":1458728470000},"page":"57-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Towards a Certified Version of the Encyclopedia of Triangle Centers"],"prefix":"10.1007","volume":"10","author":[{"given":"Julien","family":"Narboux","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Braun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,3,23]]},"reference":[{"key":"254_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Texts in Theoretical Computer Science. An EATCS Series (2004)"},{"key":"254_CR2","first-page":"89","volume-title":"Post-proceedings of Automated Deduction in Geometry 2012 volume 7993 of LNCS","author":"G Braun","year":"2012","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Post-proceedings of Automated Deduction in Geometry 2012 volume 7993 of LNCS, pp. 89\u2013109. Springer, Edinburgh (2012)"},{"key":"254_CR3","unstructured":"Boutry, P., Narboux, J., Schreck, P., Braun, G.: Automated Deduction in Geometry 2014. Proceedings of ADG 2014. In: Botana, Francisco, Quaresma, Pedro (eds.) Using small scale automation to improve both accessibility and readability of formal proofs in geometry. pp 1\u201319, Coimbra, Portugal (2014)"},{"key":"254_CR4","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S.: Ritt-Wu\u2019s Decomposition Algorithm and Geometry Theorem Proving. In: Stickel, Mark\u00a0E. (eds.) CADE, volume 449 of Lecture Notes in Computer Science. pp 207\u2013220, Springer (1990)","DOI":"10.1007\/3-540-52885-7_89"},{"key":"254_CR5","unstructured":"Delahaye, D., Mayero, M.: Field, une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en coq. In: JFLA, pp. 33\u201348 (2001)"},{"key":"254_CR6","unstructured":"Gallatly, W.: The modern geometry of the triangle. In: Hodgson, F (ed) London (1910)"},{"key":"254_CR7","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in coq. In: Hurd, J., Melham, Thomas F.: (eds), Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22\u201325, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science. Springer, pp. 98\u2013113 (2005)","DOI":"10.1007\/11541868_7"},{"key":"254_CR8","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry Theorem Proving using Hilbert\u2019s Nullstellensatz. In: SYMSAC \u201986: Proceedings of the fifth ACM symposium on Symbolic and algebraic computation. pp 202\u2013208, ACM Press, New York (1986)","DOI":"10.1145\/32439.32479"},{"key":"254_CR9","doi-asserted-by":"crossref","unstructured":"Kimberling, C.: Triangle centers as functions. J. Math. 23(4) (1993)","DOI":"10.1216\/rmjm\/1181072493"},{"key":"254_CR10","doi-asserted-by":"crossref","unstructured":"Kimberling, C.: Central points and central lines in the plane of a triangle. Math Mag, pp 163\u2013187 (1994)","DOI":"10.2307\/2690608"},{"key":"254_CR11","unstructured":"Kimberling, C.: Triangle centers and central triangles (1998)"},{"key":"254_CR12","doi-asserted-by":"crossref","unstructured":"Narboux, J.: Mechanical Theorem Proving in Tarski\u2019s geometry. In: Eugenio, Francisco\u00a0Botana, Lozano, Roanes: (eds.) Post-proceedings of Automated Deduction in Geometry 2006, vol 4869 of LNCS, Pontevedra, Spain, Francisco Botana, pp 139\u2013156. Springer (2007)","DOI":"10.1007\/978-3-540-77356-6_9"},{"issue":"6","key":"254_CR13","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1016\/S0747-7171(03)00032-4","volume":"35","author":"M Rybowicz","year":"2003","unstructured":"Rybowicz, M.: On the normalization of numbers and functions defined by radicals. J. Symbol. Comput. 35(6), 651\u2013672 (2003)","journal-title":"J. Symbol. Comput."},{"issue":"1\u20132","key":"254_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01531321","volume":"13","author":"D Wang","year":"1995","unstructured":"Wang, D.: Elimination procedures for mechanical theorem proving in geometry. Ann. Math. Artif. Intell. 13(1\u20132), 1\u201324 (1995)","journal-title":"Ann. Math. Artif. Intell."},{"key":"254_CR15","unstructured":"Yiu, P.: Introduction to the geometry of triangle (2002)"},{"issue":"2","key":"254_CR16","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/S0747-7171(85)80014-6","volume":"1","author":"R Zippel","year":"1985","unstructured":"Zippel, R.: Simplification of expressions involving radicals. J. Symbol. Comput. 1(2), 189\u2013210 (1985)","journal-title":"J. Symbol. Comput."}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-016-0254-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-016-0254-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-016-0254-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T18:35:11Z","timestamp":1559414111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-016-0254-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["254"],"URL":"https:\/\/doi.org\/10.1007\/s11786-016-0254-4","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"value":"1661-8270","type":"print"},{"value":"1661-8289","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3]]}}}