{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T22:02:20Z","timestamp":1757455340293,"version":"3.37.3"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T00:00:00Z","timestamp":1673308800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T00:00:00Z","timestamp":1673308800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eanciae a Tecnologia","doi-asserted-by":"publisher","award":["CISUC - UID\/CEC\/00326\/2020"],"award-info":[{"award-number":["CISUC - UID\/CEC\/00326\/2020"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004895","name":"European Social Fund","doi-asserted-by":"publisher","award":["Regional Operational Program Centro 2020"],"award-info":[{"award-number":["Regional Operational Program Centro 2020"]}],"id":[{"id":"10.13039\/501100004895","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003407","name":"Ministero dell\u2019Istruzione, dell\u2019Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","award":["PRIN 2017 project \u201cThe Manifest Image and the Scientific Image\u201d prot. 2017ZNWW7F_004"],"award-info":[{"award-number":["PRIN 2017 project \u201cThe Manifest Image and the Scientific Image\u201d prot. 2017ZNWW7F_004"]}],"id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Using an approach, inspired by our modernisation of Lemoine\u2019s <jats:italic>Geometrography<\/jats:italic>, this paper proposes a new readability criterion for formal proofs produced by automated theorem provers for geometry. We analyse two criteria to measure the readability of a proof: the criterion given by Chou et al. and the one given by Wiedijk. After discussing the limitations of these two criteria, we introduce a novel approach, which provides a new criterion. We conclude discussing some future work.<\/jats:p>","DOI":"10.1007\/s10817-022-09652-0","type":"journal-article","created":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T08:03:11Z","timestamp":1673337791000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Measuring the Readability of Geometric Proofs: The Area Method Case"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7728-4935","authenticated-orcid":false,"given":"Pedro","family":"Quaresma","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8828-8920","authenticated-orcid":false,"given":"Pierluigi","family":"Graziani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,1,10]]},"reference":[{"key":"9652_CR1","doi-asserted-by":"publisher","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"SC Chou","year":"1994","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)"},{"key":"9652_CR2","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00283134","volume":"17","author":"SC Chou","year":"1996","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation. J. Automat. Reason. 17, 325\u2013347 (1996). https:\/\/doi.org\/10.1007\/BF00283134","journal-title":"J. Automat. Reason."},{"issue":"3","key":"9652_CR3","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BF00283134","volume":"17","author":"SC Chou","year":"1996","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles. J. Automat. Reason. 17(3), 349\u2013370 (1996). https:\/\/doi.org\/10.1007\/BF00283134","journal-title":"J. Automat. Reason."},{"key":"9652_CR4","doi-asserted-by":"publisher","unstructured":"de Bruijn, N.: Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics, vol. 133, chap. A survey of the project Automath, pp. 141\u2013161. Elsevier, Amsterdam (1994). https:\/\/doi.org\/10.1016\/S0049-237X(08)70203-9","DOI":"10.1016\/S0049-237X(08)70203-9"},{"key":"9652_CR5","unstructured":"DuBay, W.H. (ed.): The Classic Readability Studies. Impact Information (2006)"},{"key":"9652_CR6","doi-asserted-by":"publisher","unstructured":"Gao, H., Li, J., Cheng, J.: Measuring interestingness of theorems in automated theorem finding by forward reasoning based on strong relevant logic. In: 2019 IEEE International Conference on Energy Internet (ICEI), pp. 356\u2013361 (2019). https:\/\/doi.org\/10.1109\/ICEI.2019.00069","DOI":"10.1109\/ICEI.2019.00069"},{"volume-title":"Proof Technology in Mathematics Research and Teaching","year":"2019","key":"9652_CR7","unstructured":"Hanna, G., Reid, D., de Villiers, M. (eds.): Proof Technology in Mathematics Research and Teaching. Springer, Berlin (2019)"},{"key":"9652_CR8","unstructured":"Hohenwarter, M.: Geogebra\u2014a software system for dynamic geometry and algebra in the plane. Master\u2019s thesis, University of Salzburg, Austria (2002)"},{"key":"9652_CR9","doi-asserted-by":"publisher","unstructured":"Jani\u010di\u0107, P.: GCLC - A tool for constructive Euclidean geometry and more than that. In: A.\u00a0Iglesias, N.\u00a0Takayama (eds.) Mathematical Software - ICMS 2006, Lecture Notes in Computer Science, vol. 4151, pp. 58\u201373. Springer (2006). https:\/\/doi.org\/10.1007\/11832225_6","DOI":"10.1007\/11832225_6"},{"issue":"4","key":"9652_CR10","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/s10817-010-9209-7","volume":"48","author":"P Jani\u010di\u0107","year":"2012","unstructured":"Jani\u010di\u0107, P., Narboux, J., Quaresma, P.: The area method: a recapitulation. J. Automat. Reason. 48(4), 489\u2013532 (2012). https:\/\/doi.org\/10.1007\/s10817-010-9209-7","journal-title":"J. Automat. Reason."},{"key":"9652_CR11","doi-asserted-by":"publisher","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: System description: GCLCprover + GeoThms. In: U.\u00a0Furbach, N.\u00a0Shankar (eds.) Automated Reasoning, Lecture Notes in Computer Science, vol. 4130, pp. 145\u2013150. Springer (2006). https:\/\/doi.org\/10.1007\/11814771_13","DOI":"10.1007\/11814771_13"},{"issue":"4","key":"9652_CR12","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1007\/s11424-012-2048-3","volume":"25","author":"J Jiang","year":"2012","unstructured":"Jiang, J., Zhang, J.: A review and prospect of readable machine proofs for geometry theorems. J. Syst. Sci. Complexity 25(4), 802\u2013820 (2012). https:\/\/doi.org\/10.1007\/s11424-012-2048-3","journal-title":"J. Syst. Sci. Complexity"},{"issue":"2","key":"9652_CR13","doi-asserted-by":"publisher","first-page":"105","DOI":"10.5951\/MT.50.2.0105","volume":"50","author":"DA Johnson","year":"1957","unstructured":"Johnson, D.A.: The readability of mathematics books. Math. Teach. 50(2), 105\u2013110 (1957). https:\/\/doi.org\/10.5951\/MT.50.2.0105","journal-title":"Math. Teach."},{"key":"9652_CR14","unstructured":"Lemoine, \u00c9.: G\u00e9om\u00e9trographie ou Art des constructions g\u00e9om\u00e9triques. No.\u00a018 in Scientia, S\u00e9rie Physico-Math\u00e9matique. C. Naud, \u00c9diteur, Paris (1902). http:\/\/catalogue.bnf.fr\/ark:\/12148\/cb36049032t"},{"issue":"6","key":"9652_CR15","first-page":"114","volume":"3","author":"G Loria","year":"1908","unstructured":"Loria, G.: La geometrografia e le sue trasfigurazioni. Period. Mat. 3(6), 114\u2013122 (1908)","journal-title":"Period. Mat."},{"key":"9652_CR16","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1017\/S0013091500001565","volume":"12","author":"JS Mackay","year":"1893","unstructured":"Mackay, J.S.: The geometrography of Euclid\u2019s problems. Proc. Edinb. Math. Soc. 12, 2\u201316 (1893). https:\/\/doi.org\/10.1017\/S0013091500001565","journal-title":"Proc. Edinb. Math. Soc."},{"issue":"1","key":"9652_CR17","first-page":"15","volume":"13","author":"JK Merikoski","year":"2010","unstructured":"Merikoski, J.K., Tossavainen, T.: Two approaches to geometrography. J. Geom. Graph. 13(1), 15\u201328 (2010)","journal-title":"J. Geom. Graph."},{"key":"9652_CR18","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/b100400","volume":"3223","author":"J Narboux","year":"2004","unstructured":"Narboux, J.: A decision procedure for geometry in Coq. Lect. Notes Comput. Sci. 3223, 225\u2013240 (2004). https:\/\/doi.org\/10.1007\/b100400","journal-title":"Lect. Notes Comput. Sci."},{"key":"9652_CR19","unstructured":"Pak, K., Schubert, A.: The impact of proof steps sequence on proof readability\u2014experimental setting. In: Workshop and Work in Progress Papers at CICM 2016 (2016)"},{"key":"9652_CR20","unstructured":"Pinheiro, V.A.: Geometrografia 1. Gr\u00e1fica Editora Bahiense (1974)"},{"key":"9652_CR21","unstructured":"Quaresma, P., Graziani, P.: The geometrography\u2019s simplicity coefficient for the axioms and lemma of the area method. Technical Report TR 2021-001, Center for Informatics and Systems of the University of Coimbra (2021)"},{"key":"9652_CR22","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.jsc.2018.12.004","volume":"97","author":"P Quaresma","year":"2020","unstructured":"Quaresma, P., Santos, V., Graziani, P., Baeta, N.: Taxonomy of geometric problems. J. Symbol. Comput. 97, 31\u201355 (2020). https:\/\/doi.org\/10.1016\/j.jsc.2018.12.004","journal-title":"J. Symbol. Comput."},{"key":"9652_CR23","doi-asserted-by":"publisher","unstructured":"Richard, P., V\u00e9lez, M., Vaerenbergh, S.V. (eds.): Mathematics Education in the Age of Artificial Intelligence, Mathematics Education in the Digital Era, vol.\u00a017. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-86909-0","DOI":"10.1007\/978-3-030-86909-0"},{"issue":"2","key":"9652_CR24","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1564\/tme_v26.2.06","volume":"26","author":"V Santos","year":"2019","unstructured":"Santos, V., Baeta, N., Quaresma, P.: Geometrography in dynamic geometry. Int. J. Technol. Math. Educ. 26(2), 89\u201396 (2019). https:\/\/doi.org\/10.1564\/tme_v26.2.06","journal-title":"Int. J. Technol. Math. Educ."},{"key":"9652_CR25","doi-asserted-by":"publisher","unstructured":"Stojanovi\u0107, S., Pavlovi\u0107, V., Jani\u010di\u0107, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: P.\u00a0Schreck, J.\u00a0Narboux, J.\u00a0Richter-Gebert (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6877, pp. 201\u2013220. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-25070-5_12","DOI":"10.1007\/978-3-642-25070-5_12"},{"key":"9652_CR26","unstructured":"Wang, K., Su, Z.: Automated geometry theorem proving for human-readable proofs. In: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI\u201915, pp. 1193\u20131199. AAAI (2015). http:\/\/dl.acm.org\/citation.cfm?id=2832249.2832414"},{"key":"9652_CR27","unstructured":"Wiedijk, F.: The de Bruijn factor. Poster at International Conference on Theorem Proving in Higher Order Logics (TPHOL2000) (2000). Portland, Oregon, USA, 14\u201318 August 2000"},{"issue":"3","key":"9652_CR28","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10817-009-9163-4","volume":"45","author":"Z Ye","year":"2010","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. J. Automat. Reason. 45(3), 243\u2013266 (2010). https:\/\/doi.org\/10.1007\/s10817-009-9163-4","journal-title":"J. Automat. Reason."},{"key":"9652_CR29","doi-asserted-by":"publisher","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: An introduction to Java geometry expert. In: T.\u00a0Sturm, C.\u00a0Zengler (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6301, pp. 189\u2013195. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-21046-4_10","DOI":"10.1007\/978-3-642-21046-4_10"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09652-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09652-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09652-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,24]],"date-time":"2023-03-24T09:23:47Z","timestamp":1679649827000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09652-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,10]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["9652"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09652-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,1,10]]},"assertion":[{"value":"20 January 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 September 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 January 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 March 2023","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Missing Open Access funding information has been added in the Funding Note.","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"5"}}