{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:03:31Z","timestamp":1760061811483},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2007,6,30]],"date-time":"2007-06-30T00:00:00Z","timestamp":1183161600000},"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":[[2007,8,20]]},"DOI":"10.1007\/s10817-007-9071-4","type":"journal-article","created":{"date-parts":[[2007,6,29]],"date-time":"2007-06-29T09:58:05Z","timestamp":1183111085000},"page":"161-180","source":"Crossref","is-referenced-by-count":31,"title":["A Graphical User Interface for Formal Proofs in Geometry"],"prefix":"10.1007","volume":"39","author":[{"given":"Julien","family":"Narboux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,6,30]]},"reference":[{"key":"9071_CR1","unstructured":"Ag-Almouloud, S.: L\u2019ordinateur, outil d\u2019aide \u00e0 l\u2019apprentissage de la d\u00e9monstration et de traitement de donn\u00e9es didactiques. Ph.D. thesis, Universit\u00e9 de Rennes (1992)"},{"key":"9071_CR2","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 (2001)"},{"key":"9071_CR3","unstructured":"Anderson, J.R., Boyle, C.F., Yost, G.: The geometry tutor. In: IJCAI Proceedings, pp. 1\u20137 (1985)"},{"key":"9071_CR4","unstructured":"Aspinall, D., L\u00fcth, C., Winterstein, D.: A framework for interactive proof. Technical report (2004)"},{"key":"9071_CR5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"9071_CR6","unstructured":"Balacheff, N., Pesty, S., Occello, M., Caffera, R., Webber, C., Peltier, N.: Baghera. http:\/\/www-baghera.imag.fr (1999\u20132002)"},{"key":"9071_CR7","doi-asserted-by":"crossref","unstructured":"Barwise, J., Allwein, G. (eds.): Logical Reasoning with Diagrams. Oxford University Press (1996)","DOI":"10.1093\/oso\/9780195104271.001.0001"},{"key":"9071_CR8","unstructured":"Bernat, P.: CHYPRE: Un logiciel d\u2019aide au raisonnement. Technical report\u00a010, IREM (1993)"},{"key":"9071_CR9","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/j.entcs.2004.09.013","volume":"103","author":"Y. Bertot","year":"2003","unstructured":"Bertot, Y., Guilhot, F., Pottier, L.: Visualizing geometrical statements with GeoView. Electronic Notes in Theoretical Computer Science 103, 49\u201365 (2003)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9071_CR10","doi-asserted-by":"crossref","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. J. Symb. Comput. 25, 161\u2013194 (1998)","journal-title":"J. Symb. Comput."},{"key":"9071_CR11","doi-asserted-by":"crossref","unstructured":"Chou, S.-C.: Mechanical geometry theorem proving. Reidel (1988)","DOI":"10.1007\/978-94-009-4037-6"},{"key":"9071_CR12","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S.: A class of geometry statements of constructive type and geometry theorem proving. In: Proceedings of CADE\u201992 (1992)","DOI":"10.1007\/3-540-55602-8_153"},{"key":"9071_CR13","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"S.-C. Chou","year":"1994","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. Singapore: World Scientific. (1994)"},{"key":"9071_CR14","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","volume":"17","author":"S.-C. Chou","year":"1996","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants, theorem proving with full angle. J. Autom. Reason. 17, 325\u2013347 (1996)","journal-title":"J. Autom. Reason."},{"key":"9071_CR15","unstructured":"Coq development team: The Coq proof assistant reference manual. Version 8.0. LogiCal Project (2004)"},{"key":"9071_CR16","unstructured":"Furinghetti, F., Domingo, P.: To produce conjectures and to prove them within a dynamic geometry environment: a case study. In: Proceedings of Psychology of Mathematics 27th International Conference, pp. 397\u2013404 (2003)"},{"key":"9071_CR17","unstructured":"Gao, X.-S.: Geometry expert, software package. http:\/\/www.mmrc.iss.ac.cn\/gex (2000)"},{"key":"9071_CR18","doi-asserted-by":"crossref","unstructured":"Gao, X.-S., Lin, Q.: MMP\/Geometer \u2013 a software package for automated geometry reasoning. In: Winkler, F. (ed.) Proceedings of ADG 2002, pp. 44\u201346 (2002)","DOI":"10.1007\/978-3-540-24616-9_4"},{"key":"9071_CR19","unstructured":"Gressier, J.: Geometrix. http:\/\/perso.orange.fr\/jgressier\/ENGLISH\/english.html (1988\u20131998)"},{"key":"9071_CR20","doi-asserted-by":"crossref","unstructured":"Guilhot, F.: Formalisation en Coq et visualisation d\u2019un cours de g\u00e9om\u00e9trie pour le lyc\u00e9e. Revue des Sciences et Technologies de l\u2019Information, Technique et Science Informatiques, Langages applicatifs 24, 1113\u20131138 (2005) Lavoisier.","DOI":"10.3166\/tsi.24.1113-1138"},{"key":"9071_CR21","unstructured":"Harrison, J.: Automatic theorem proving examples. http:\/\/www.cl.cam.ac.uk\/users\/jrh\/atp\/index.html (2003)"},{"key":"9071_CR22","unstructured":"Jackiw, N.: The geometer\u2019s sketchpad. http:\/\/www.keypress.com\/ (1990)"},{"key":"9071_CR23","unstructured":"Jamnik, M.: Mathematical Reasoning with Diagrams: From Intuition to Automation. CSLI Press. (2001)"},{"key":"9071_CR24","unstructured":"Kortenkamp, U.: Foundations of dynamic geometry. Ph.D. thesis, ETH Z\u00fcrich (1999)"},{"key":"9071_CR25","unstructured":"Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Mathematical User Interface (2004)"},{"key":"9071_CR26","unstructured":"Laborde, J.-M., Bellemain, F.: Cabri-geometry II. http:\/\/www.cabri.net (1993\u20131998)"},{"key":"9071_CR27","unstructured":"Luengo, V.: Cabri-Euclide: Un micromonde de Preuve int\u00e9grant la r\u00e9futation. Ph.D. thesis, Universit\u00e9 Joseph Fourier (1997)"},{"key":"9071_CR28","doi-asserted-by":"crossref","unstructured":"Meikle, L., Fleuriot, J.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Theorem Proving in Higher Order Logics, pp. 319\u2013334 (2003)","DOI":"10.1007\/10930755_21"},{"key":"9071_CR29","unstructured":"Miller, N.: A diagrammatic formal system for Euclidean geometry. Ph.D. thesis, Cornell University (2001)"},{"key":"9071_CR30","doi-asserted-by":"crossref","unstructured":"Narboux, J.: A decision procedure for geometry in Coq. In: Konrad, S., Annett, B., Ganesh, G. (eds.) Proceedings of TPHOLs\u2019 2004, vol. 3223 of Lecture Notes in Computer Science (2004)","DOI":"10.1007\/978-3-540-30142-4_17"},{"key":"9071_CR31","unstructured":"Narboux, J.: Formalisation et automatisation du raisonnement g\u00e9om\u00e9trique en Coq\u2019. Ph.D. thesis, Universit\u00e9 Paris Sud (2006a)"},{"key":"9071_CR32","unstructured":"Narboux, J.: A formalization of diagrammatic proofs in abstract rewriting (2006b)"},{"key":"9071_CR33","unstructured":"Narboux, J.: Mechanical theorem proving in Tarski\u2019s geometry. In: Proceedings of Automatic Deduction in Geometry 06 (2006c)"},{"key":"9071_CR34","unstructured":"Narboux, J.: The user manual of GeoProof. http:\/\/home.gna.org\/geoproof\/documentation.html (2006d)"},{"key":"9071_CR35","unstructured":"Py, D.: Reconnaissance de plan pour l\u2019aide \u00e0 la d\u00e9monstration dans un tuteur intelligent de la g\u00e9om\u00e9trie. Ph.D. thesis, Universit\u00e9 de Rennes (1990)"},{"key":"9071_CR36","doi-asserted-by":"crossref","unstructured":"Richter-Gebert, J., Kortenkamp, U.: Die interaktive Geometrie software Cinderella Book and CD-ROM. German school-edition of the Cinderella software. http:\/\/cinderella.de (1999)","DOI":"10.1007\/978-3-642-58318-6"},{"key":"9071_CR37","doi-asserted-by":"crossref","unstructured":"Schwartz, J. T.: Probabilistic algorithms for verification of polynomial identities. In: Symbolic and Algebraic Computation, vol.\u00a072. Lecture Notes in Computer Science. Marseille, pp. 200\u2013215 (1979)","DOI":"10.1007\/3-540-09519-5_72"},{"key":"9071_CR38","unstructured":"Wilson, S., Fleuriot, J.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In: ETAPS Satellite Workshop on User Interfaces for Theorem Provers (UITP). Edinburgh (2005)"},{"key":"9071_CR39","doi-asserted-by":"crossref","unstructured":"Winterstein, D.: Dr. Doodle: A diagrammatic theorem prover. In: Proceedings of IJCAR 2004 (2004a)","DOI":"10.1007\/978-3-540-25984-8_24"},{"key":"9071_CR40","unstructured":"Winterstein, D.: Using diagrammatic reasoning for theorem proving in continous domain. Ph.D. thesis, The University of Edinburgh (2004b)"},{"key":"9071_CR41","unstructured":"Winterstein, D., Aspinall, D., L\u00fcth, C.: PG\/Eclipse: A generic interface for interactive proof. Technical report (2004)"},{"key":"9071_CR42","unstructured":"Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. In: Scientia Sinica, vol.\u00a021. pp. 157\u2013179 (1978)"},{"key":"9071_CR43","unstructured":"Yevdokimov, O.: About a constructivist approach for stimulating students\u2019 thinking to produce conjectures and their proving in active learning of geometry. In: Fourth Congress of the European Society for Research in Mathematics Education (2004)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9071-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9071-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9071-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T19:08:10Z","timestamp":1683918490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9071-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,30]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,8,20]]}},"alternative-id":["9071"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9071-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6,30]]}}}