{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:59:05Z","timestamp":1766138345477,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T00:00:00Z","timestamp":1688342400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T00:00:00Z","timestamp":1688342400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2023,12]]},"DOI":"10.1007\/s10472-023-09857-y","type":"journal-article","created":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T05:01:20Z","timestamp":1688360480000},"page":"797-820","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated generation of illustrated proofs in geometry and beyond"],"prefix":"10.1007","volume":"91","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8922-4948","authenticated-orcid":false,"given":"Predrag","family":"Jani\u010di\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3527-7184","authenticated-orcid":false,"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,3]]},"reference":[{"key":"9857_CR1","unstructured":"Amerkad, A., Bertot, Y., Pottier L., Rideau, L.:Mathematics and proof presentation in pcoq. In Workshop Proof Transformation and Presentation and Proof Complexities in connection with IJCAR 2001, Siena, June 2001"},{"key":"9857_CR2","doi-asserted-by":"publisher","first-page":"700","DOI":"10.1017\/S1755020309990098","volume":"2","author":"J Avigad","year":"2009","unstructured":"Avigad, J., Dean, E., Mumma, J.: A formal system for euclid\u2019s elements. The Review of Symbolic Logic. 2, 700\u2013768 (2009)","journal-title":"The Review of Symbolic Logic."},{"key":"9857_CR3","doi-asserted-by":"crossref","unstructured":"Beeson, M., Narboux, J., Wiedijk F.:Proof-checking euclid. Annals of Mathematics and Artificial Intelligence. 85(2-4), 213\u2013257. Publisher: Springer (2019)","DOI":"10.1007\/s10472-018-9606-x"},{"issue":"103","key":"9857_CR4","first-page":"49","volume":"2003","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Guilhot, F., Pottier, L.: Visualizing geometrical statements with geoView. Proceedings of the Workshop User Interfaces for Theorem Provers 2003(103), 49\u201365 (2004)","journal-title":"Proceedings of the Workshop User Interfaces for Theorem Provers"},{"key":"9857_CR5","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1006\/jsco.1997.0171","volume":"25","author":"Y Bertot","year":"1998","unstructured":"Bertot, Y., Thery, L.: A generic approach to building user interfaces for theorem provers. The Journal of Symbolic Computation. 25, 161\u2013194 (1998)","journal-title":"The Journal of Symbolic Computation."},{"key":"9857_CR6","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1142\/9789812562494_0050","volume":"2","author":"M Bezem","year":"2004","unstructured":"Bezem, M., Coquand, T.: Newman\u2019s lemma - a case study in proof automation and geometric logic. Current Trends in Theoretical Computer Science. 2, 267\u2013282 (2004)","journal-title":"Current Trends in Theoretical Computer Science."},{"key":"9857_CR7","doi-asserted-by":"crossref","unstructured":"Bezem,M., Coquand, T.:Automating coherent logic. In Sutcliffe, G., Voronkov, A. (eds.) 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR 2005, vol. 3835 of Lecture Notes in Computer Science, pp. 246\u2013260. Springer-Verlag (2005)","DOI":"10.1007\/11591191_18"},{"issue":"1","key":"9857_CR8","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10817-015-9326-4","volume":"55","author":"F Botana","year":"2015","unstructured":"Botana, F., Hohenwarter, M., Jani\u010di\u0107, P., Kov\u00e1cs, Z., Petrovi\u0107, I., Recio, T., Weitzhofer, S.: Automated theorem proving in geoGebra:current achievements. Journal of Automated Reasoning. 55(1), 39\u201359 (2015)","journal-title":"Journal of Automated Reasoning."},{"key":"9857_CR9","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.:Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles. Journal of Automated Reasoning. 17(13), 349\u2013370 (1996)","DOI":"10.1007\/BF00283134"},{"key":"9857_CR10","doi-asserted-by":"crossref","unstructured":"Shang-Ching, C., Xiao-Shan, G.:A survey of geometric reasoning using algebraic methods. pp. 97\u2013119. Birkh\u00e4user Boston, Boston, MA (1996)","DOI":"10.1007\/978-1-4612-4088-4_5"},{"key":"9857_CR11","unstructured":"Coq development team, The. The Coq proof assistant reference manual, Version 8.3. LogiCal Project (2010)"},{"key":"9857_CR12","unstructured":"Coquand, t., Huet, G.:Concepts mathematiques et informatiques formalises dans le calcul des constructions. Technical Report RR-0463, INRIA, December 1985"},{"key":"9857_CR13","unstructured":"Duval, R., Egret, M.A.: Introduction \u00e1 la d \u00e8monstration et apprentissage du raisonnement d \u00e8ductif. Rep \u00e8res-IREM. 12, 114\u2013140 (July1993)"},{"key":"9857_CR14","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/bsl.2015.7","volume":"21","author":"R Dyckhoff","year":"2015","unstructured":"Dyckhoff, R., Negri, S.: Geometrization of first-order logic. The Bulletin of Symbolic Logic. 21, 123\u2013163 (2015)","journal-title":"The Bulletin of Symbolic Logic."},{"key":"9857_CR15","unstructured":"Ganesalingam, M., Gowers, W.T.:A fully automatic problem solver with human-style output. CoRR, abs\/1309.4501, 2013"},{"key":"9857_CR16","doi-asserted-by":"crossref","unstructured":"Gao, X.S., Lin, Q.:MMP\/geometer - A software package for automated geometric reasoning. In Proceedings of Automated Deduction in Geometry (ADG02). vol.2930 of Lecture Notes in Computer Science pp. 44\u201366. Springer-Verlag (2004)","DOI":"10.1007\/978-3-540-24616-9_4"},{"key":"9857_CR17","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hansen, J.R., Loveland, D.: Empirical explorations of the geometry theorem machine. In Papers presented at the May 3-5, 1960, western joint IRE-AIEE-ACM computer conference, IRE-AIEE-ACM \u201960 (Western), pp. 143\u2013149. San Francisco, California, 1960. ACM","DOI":"10.1145\/1460361.1460381"},{"issue":"4","key":"9857_CR18","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions:abstract properties and applications to term rewriting systems. Journal of the ACM. 27(4), 797\u2013821 (1980)","journal-title":"Journal of the ACM."},{"key":"9857_CR19","doi-asserted-by":"crossref","unstructured":"Janicic, P., Narboux, J.:Automated generation of illustrations for synthetic geometry proofs. In Predrag Janicic and Zolt\u00e1n Kov\u00e1cs, editors, Proceedings of the 13th International Conference on Automated Deduction in Geometry, ADG 2021, Hagenberg, Austria\/virtual, September 15-17, 2021, vol. 352 of EPTCS, pp. 91\u2013102 (2021)","DOI":"10.4204\/EPTCS.352.9"},{"key":"9857_CR20","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P., Narboux, J.:Theorem proving as constraint solving with coherent logic. Journal of Automated Reasoning, 2022. To appear","DOI":"10.1007\/s10817-022-09629-z"},{"key":"9857_CR21","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P.:GCLC - a tool for constructive euclidean geometry and more than that. In Iglesias, A., Takayama, N. (eds.) Mathematical Software - ICMS 2006. vol. 4151 of Lecture Notes in Computer Science. pp. 58\u201373. Springer (2006)","DOI":"10.1007\/11832225_6"},{"key":"9857_CR22","unstructured":"Jani\u010di \u0107, P.:GCLC 9.0\/WinGCLC 2009. Manual for the GCLC Dynamic Geometry Software. (2009)"},{"key":"9857_CR23","doi-asserted-by":"crossref","unstructured":"Jani\u010di \u0107, P.:Geometry constructions language. Journal of Automated Reasoning. 44(1-2), 3\u201324 (2010)","DOI":"10.1007\/s10817-009-9135-8"},{"key":"9857_CR24","unstructured":"Karasawa, T.:Historic investigation of legendre\u2019s proof about the 5th postulate of \u201cElements\u201c for reeducation of mathematics teacher. Journal of Modern Education Review. pp. 926\u2013931 December 2013"},{"key":"9857_CR25","unstructured":"Miller, N.:A diagrammatic formal system for Euclidean geometry. PhD Thesis, Cornell University. May 2001"},{"key":"9857_CR26","unstructured":"Narboux, J.:A formalization of diagrammatic proofs in abstract rewriting. working paper or preprint, 2006"},{"issue":"2","key":"9857_CR27","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-007-9071-4","volume":"39","author":"J Narboux","year":"2007","unstructured":"Narboux, J.: A graphical user interface for formal proofs in geometry. Journal of Automated Reasoning. 39(2), 161\u2013180 (2007)","journal-title":"Journal of Automated Reasoning."},{"key":"9857_CR28","doi-asserted-by":"crossref","unstructured":"Narboux, J., Durand-Guerrier, V.:Combining pencil\/paper proofs and formal proofs, a challenge for artificial intelligence and mathematics education. In Mathematics Education in the Age of Artificial Intelligence: How Intelligence can serve mathematical human learning. Springer (2021, In press)","DOI":"10.1007\/978-3-030-86909-0_8"},{"key":"9857_CR29","doi-asserted-by":"crossref","unstructured":"de Nivelle, H., Meng, J.:Geometric resolution:a proof procedure based on finite model search. In Furbach, U., Shankar, N. (eds.) Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, vol. 4130 of Lecture Notes in Computer Science. pp. 303\u2013317. Springer (2006)","DOI":"10.1007\/11814771_28"},{"key":"9857_CR30","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2012.06.005","volume":"285","author":"TM Pham","year":"2012","unstructured":"Pham, T.M., Bertot, Y.: A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. Electron. Notes Theor. Comput. Sci. 285, 43\u201355 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9857_CR31","unstructured":"Polonsky, A.:Proofs, types and lambda calculus. PhD Thesis, University of Bergen (2011)"},{"key":"9857_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische methoden in der geometrie","author":"W Schwabh\u00e4user","year":"1983","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische methoden in der geometrie. Springer-Verlag, Berlin (1983)"},{"key":"9857_CR33","doi-asserted-by":"crossref","unstructured":"Stojanovi\u0107, S., Narboux, J., Bezem, M., Jani\u010di \u0107, P.:A vernacular for coherent logic. In Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics. vol. 8543 of Lecture Notes in Computer Science. pp. 388\u2013403 Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-08434-3_28"},{"key":"9857_CR34","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.:The TPTP problem library and associated infrastructure:the FOF and CNF parts. v3.5.0. Journal of Automated Reasoning. 43(4), 337\u2013362 (2009)","DOI":"10.1007\/s10817-009-9143-8"},{"key":"9857_CR35","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-662-05148-1_15","volume-title":"Algebra, geometry and software systems","author":"D Wang","year":"2003","unstructured":"Wang, D.: Automated generation of diagrams with maple and java. In: Joswig, M., Takayama, N. (eds.) Algebra, geometry and software systems, pp. 277\u2013287. Springer, Berlin, Heidelberg (2003)"},{"key":"9857_CR36","volume-title":"Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs","author":"S Wilson","year":"2005","unstructured":"Wilson, S., Fleuriot, J.D.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. Springer, In ETAPS Satellite Workshop on User Interfaces for Theorem Provers(UITP), Edinburgh (2005)"},{"key":"9857_CR37","doi-asserted-by":"crossref","unstructured":"Winterstein, D.:Dr. Doodle:A diagrammatic theorem prover. In Proceedings of IJCAR 2004. (2004)","DOI":"10.1007\/978-3-540-25984-8_24"},{"key":"9857_CR38","doi-asserted-by":"crossref","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry, part 1 basic features and the manual input method. Journal of Automated Reasoning. 45(3), 213\u2013241 (Oct2010)","DOI":"10.1007\/s10817-009-9162-5"},{"key":"9857_CR39","doi-asserted-by":"crossref","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry, part 2 automated generation of visually dynamic presentations with the full-angle method and the deductive database method. Journal of Automated Reasoning. 45(3), 243\u2013266 (Dec2010)","DOI":"10.1007\/s10817-009-9163-4"},{"key":"9857_CR40","doi-asserted-by":"crossref","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.:An introduction to java geometry expert. In Post-proceedings of Automated Deduction in Geometry (ADG 2008). vol. 6301 of Lecture Notes in Computer Science. pp. 189\u2013195 Springer-Verlag (2011)","DOI":"10.1007\/978-3-642-21046-4_10"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-023-09857-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-023-09857-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-023-09857-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T11:08:02Z","timestamp":1700046482000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-023-09857-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,3]]},"references-count":40,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["9857"],"URL":"https:\/\/doi.org\/10.1007\/s10472-023-09857-y","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2023,7,3]]},"assertion":[{"value":"9 May 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 July 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declaration"}},{"value":"All authors certify that they have no affiliations with or involvement in any organization or entity with any financial interest or non-financial interest in the subject matter or materials discussed in this manuscript. The first author of this paper is a co-editor of the special issue this paper is submitted to, hence this submission is handled by the editor in chief.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest\/Competing interests"}}]}}