{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:58:59Z","timestamp":1760061539372,"version":"3.37.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,12,18]],"date-time":"2009-12-18T00:00:00Z","timestamp":1261094400000},"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":[[2010,10]]},"DOI":"10.1007\/s10817-009-9162-5","type":"journal-article","created":{"date-parts":[[2009,12,17]],"date-time":"2009-12-17T11:21:13Z","timestamp":1261048873000},"page":"213-241","source":"Crossref","is-referenced-by-count":22,"title":["Visually Dynamic Presentation of Proofs in Plane Geometry"],"prefix":"10.1007","volume":"45","author":[{"given":"Zheng","family":"Ye","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shang-Ching","family":"Chou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,12,18]]},"reference":[{"key":"9162_CR1","unstructured":"Nelsen, R.B.: Proofs without Words: Exercises in Visual Thinking (Classroom Resource Material) (1993)"},{"key":"9162_CR2","unstructured":"Nelsen, R.B.: Proofs without Words II: more Exercises in Visual Thinking (Classroom Resource Material), by Roger B. Nelsen (2001)"},{"key":"9162_CR3","doi-asserted-by":"crossref","DOI":"10.5948\/UPO9781614441007","volume-title":"[C] Math Made Visual: Creating Images For Understanding Mathematics","author":"C Alsina","year":"2006","unstructured":"Alsina, C., Nelsen, R.B.: [C] Math Made Visual: Creating Images For Understanding Mathematics. The Mathematical Association of America, New York (2006)"},{"key":"9162_CR4","unstructured":"Cut-The-Knot: Geometry articles, theorems, problems. http:\/\/www.cut-the-knot.org\/geometry.shtml (2009)"},{"key":"9162_CR5","unstructured":"Cut-The-Knot: Pythagorean theorem. http:\/\/www.cut-the-knot.org\/pythagoras\/index.shtml (2009)"},{"key":"9162_CR6","unstructured":"Gao, X.S., Zhang, J.Z., Chou, S.C.: Geometry Expert. Nine Chapters Pub. (in Chinese) (1998)"},{"key":"9162_CR7","first-page":"235","volume-title":"Proc. CADE-13","author":"SC Chou","year":"1996","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: An introduction to geometry expert. In: McRobbie, M.A., Slaney, J.K. (eds.) Proc. CADE-13, pp. 235\u2013239. Springer, New York (1996)"},{"key":"9162_CR8","volume-title":"Proc. ASCM99","author":"XS Gao","year":"1999","unstructured":"Gao, X.S.: Building dynamic mathematical models with geometry expert, III. A geometry deductive database. In: Yang, W., Wang, D. (eds.) Proc. ASCM99. ATCM, Chadstone Centre (1999)"},{"key":"9162_CR9","doi-asserted-by":"crossref","unstructured":"Gao, X.S., Lin, Q.: MMP\/Geometer\u2014a software package for automated geometry reasoning. In: Winkler, F. (ed.) Automated Deduction in Geometry, pp. 44\u201366 (2004)","DOI":"10.1007\/978-3-540-24616-9_4"},{"key":"9162_CR10","unstructured":"Chou, S.C., Gao, X.S., Ye, Z.: Java geometry expert server: http:\/\/woody.cs.wichita.edu (2009) (One can run the most part of JGEX with a browser.)"},{"key":"9162_CR11","unstructured":"Les Editions du Kangourou: Le th\u00e9or\u00e8me de Th\u00e1les. http:\/\/www.mathkang.org\/swf\/thales2.html (2009)"},{"key":"9162_CR12","doi-asserted-by":"crossref","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":"9162_CR13","unstructured":"Sktektee, S., Jackiw, N., Chanan, S.: Geometer\u2019s Sketchpad Verison 4.0, Reference Manual. Key Curriculum, Emeryville (2001)"},{"key":"9162_CR14","unstructured":"Laborde, J.M., et al.: Cabri II Plus (2000)"},{"key":"9162_CR15","volume-title":"User Manual for the Interactive Geometry Software Cinderella","author":"U Kortenkamp","year":"2000","unstructured":"Kortenkamp, U., Richter-Gebert, J.: User Manual for the Interactive Geometry Software Cinderella. Springer, New York (2000)"},{"key":"9162_CR16","volume-title":"Mechanical Geometry Theorem Proving","author":"SC Chou","year":"1988","unstructured":"Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel, Dordrecht (1988)"},{"key":"9162_CR17","doi-asserted-by":"crossref","first-page":"486","DOI":"10.2307\/2975739","volume":"90","author":"KB Taylor","year":"1983","unstructured":"Taylor, K.B.: Three circles with collinear centres, solution of advanced problem 3887. Am. Math. Mon. 90, 486\u2013487 (1983)","journal-title":"Am. Math. Mon."},{"key":"9162_CR18","volume-title":"Shadows of the Mind","author":"R Penrose","year":"1994","unstructured":"Penrose, R.: Shadows of the Mind. Oxford University Press, Oxford (1994)"},{"key":"9162_CR19","unstructured":"Chou, S.C., Gao, X.S., Ye, Z.: Java geometry expert. In: Proceedings of 10th Asian Technology Conference in Mathematics, pp. 78\u201384 (2005)"},{"key":"9162_CR20","unstructured":"Chou, S.C., Gao, X.S.: A Class of Geometry Statments of Constructive Type and Geometry Theorem Proving, TR-89-37. Department of Computer Sciences, University of Texas at Austin, 32 p., November (1989)"},{"key":"9162_CR21","volume-title":"Modern Geometry","author":"CF Adler","year":"1958","unstructured":"Adler, C.F.: Modern Geometry. McGraw-Hill Book, Sydney (1958)"},{"key":"9162_CR22","volume-title":"Geometry Revisited, (New Mathematical Library)","author":"HSM Coxeter","year":"1975","unstructured":"Coxeter, H.S.M., Greitzer, S.L.: Geometry Revisited, (New Mathematical Library). The Mathematical Association of America, New York (1975)"},{"key":"9162_CR23","unstructured":"Hadamard, J.: Lecons de Geometrie Elementaire, I. Paris (1931)"},{"key":"9162_CR24","first-page":"159","volume":"21","author":"WT Wu","year":"1978","unstructured":"Wu, W.T.: On the decision problem and the mechanization of theorem in elementary geometry. Scientia Sinica 21, 159\u2013172 (1978); Automated theorem proving: after 25 years. A.M.S., Contemp. Math. 29, 213\u2013234 (1984)","journal-title":"Scientia Sinica"},{"key":"9162_CR25","unstructured":"Wu, W.T.: Basic Principles of Mechanical Theorem Proving in Geometries. Press, Beijing (in Chinese) (1984). (English Version, Springer-Verlag (1993))"},{"key":"9162_CR26","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert\u2019s Nullstellensatz. In: Proc. of SYMSAC\u201986, pp. 202\u2013208. Waterloo (1986)","DOI":"10.1145\/32439.32479"},{"key":"9162_CR27","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF02328448","volume":"4","author":"SC Chou","year":"1986","unstructured":"Chou, S.C., Schelter, W.F.: Proving geometry theorem with rewrite rules. J. Autom. Reason. 4, 253\u2013273 (1986)","journal-title":"J. Autom. Reason."},{"key":"9162_CR28","doi-asserted-by":"crossref","unstructured":"Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger\u2019s algorithm. In: Proc. of SYMSAC\u201986, pp. 209\u2013214. Waterloo (1986)","DOI":"10.1145\/32439.32480"},{"key":"9162_CR29","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hanson, J.R., Loveland, D.W.: Empirical explorations of the geometry-theorem proving machine. In: Proc. West. Joint Computer Conf., pp. 143\u2013147 (1960)","DOI":"10.1145\/1460361.1460381"},{"key":"9162_CR30","first-page":"134","volume-title":"Computers and Thought","author":"H Gelernter","year":"1963","unstructured":"Gelernter, H.: Realization of a geometry-theorem proving machine, In: Feigenbaum, E.A., Feldman, J. (eds.) Computers and Thought, pp. 134\u2013152. Mcgraw Hill, London (1963)"},{"issue":"1","key":"9162_CR31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"AJ Nevins","year":"1975","unstructured":"Nevins, A.J.: Plane geometry theorem proving using forward chaining. Artif. Intell. 6(1), 1\u201323 (1975)","journal-title":"Artif. Intell."},{"issue":"4","key":"9162_CR32","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H Coelho","year":"1986","unstructured":"Coelho, H., Pereira, L.M.: Automated reasoning in geometry theorem proving with prolog. J. Autom. Reason. 2(4), 329\u2013390 (1986)","journal-title":"J. Autom. Reason."},{"key":"9162_CR33","volume-title":"Foundations of Geometry, the first edition (in Germany) was published in 1899","author":"D Hilbert","year":"1971","unstructured":"Hilbert, D.: Foundations of Geometry, the first edition (in Germany) was published in 1899. Open Court, La Salla (1971)"},{"key":"9162_CR34","doi-asserted-by":"crossref","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 of readable proofs with geometric invariants, II. Proving theorems with full-angles. J. Autom. Reason. 17, 349\u2013370 (1996)","journal-title":"J. Autom. Reason."},{"key":"9162_CR35","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: A collection of 110 geometry theorems and their machine produced proofs using full-angles. WSU technical report (1995)","DOI":"10.1142\/9789812831699_0004"},{"issue":"3","key":"9162_CR36","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"SC Chou","year":"2000","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reas. 25(3), 219\u2013246 (2000)","journal-title":"J. Autom. Reas."},{"key":"9162_CR37","volume-title":"Mathematical Reasoning with Diagrams: From Intuition to Automation","author":"M Jamnik","year":"2001","unstructured":"Jamnik, M.: Mathematical Reasoning with Diagrams: From Intuition to Automation. CSLI, Stanford University, Stanford (2001)"},{"key":"9162_CR38","unstructured":"Guilhot, F.: Premiers pas vers un Cours de G\u00e9om\u00e9trie on Coq pour le Lyc\u00e9e. Research Report N\u00b0 4893, 44 pages, INRIA (2003)"},{"key":"9162_CR39","series-title":"LNAI","first-page":"306","volume-title":"3rd Int. Workshop on Automated Deduction in Geometry, Zurich, Switzerland, 2000","author":"C Dehlinger","year":"2001","unstructured":"Dehlinger, C., Dufourd, J.F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert\u2019s elementary geometry. In: 3rd Int. Workshop on Automated Deduction in Geometry, Zurich, Switzerland, 2000. LNAI, vol. 2061, pp. 306\u2013323. Springer, New York (2001)"},{"key":"9162_CR40","series-title":"LNAI","first-page":"139","volume-title":"Workshop on Automated Deduction in Geometry, Pontevedra, Spain, 2006","author":"J Narboux","year":"2008","unstructured":"Narboux, J.: Mechanical theorem proving in Tarski\u2019s geometry. In: Botana, F., Recio, T. (eds.) Workshop on Automated Deduction in Geometry, Pontevedra, Spain, 2006. LNAI, vol. 4869, pp. 139\u2013156. Springer, New York (2008)"},{"key":"9162_CR41","series-title":"LNCS","volume-title":"TPHOL\u201904 Proceedings","author":"J Narboux","year":"2004","unstructured":"Narboux, J.: A decision procedure for geometry in Coq. In: TPHOL\u201904 Proceedings. LNCS, vol. 3223. Springer, New York (2004)"},{"key":"9162_CR42","unstructured":"Chou, S.C., Ye, Z., Gao, X.S.: Visually Dynamic Presentation of Proofs in Plane. Part 3. Automated Generation of Visually Dynamic Presentations with the Traditional Method and Automated Addition of Auxiliary Geometry Elements (2009, in preparation)"},{"key":"9162_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/978-3-540-30210-0_8","volume-title":"Artificial Intelligence and Symbolic Computation: 7th International Conference, AISC 2004, Linz, Austria","author":"A Dolzmann","year":"2004","unstructured":"Dolzmann, A., Gilch, L.A.: Generic Hermitian quantifier elimination. In: Campbell, J.A., Buchberger, B. (eds.) Artificial Intelligence and Symbolic Computation: 7th International Conference, AISC 2004, Linz, Austria. Lecture Notes in Computer Science, vol. 3249, pp. 80\u201393. Springer, Berlin (2004)"},{"key":"9162_CR44","unstructured":"Jamnik, M., Bundy, A., Green, I.: On automating diagrammatic proofs of arithmetic arguments, In: Proceedings of International Joint Conference on AI (1997)"},{"key":"9162_CR45","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/978-3-7091-9459-1_20","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation","author":"V Weispfenning","year":"1998","unstructured":"Weispfenning, V.: A new approach to quantifier elimination for real algebra. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation, pp. 376\u2013392. Springer, Wien (1998)"},{"key":"9162_CR46","unstructured":"Winterstein, D., Bundy, A., Gurr,C.: Dr. Doodle: a diagrammatic theorem prover In: Proceedings of 2nd International Joint Conference, Cork, Ireland, pp. 331\u2013335, July 4\u20138, (2004)"},{"key":"9162_CR47","unstructured":"Winterstein, D.: Using diagrammatic reasoning for theorem proving in a continuous domain. Ph.D. thesis, 263 p., The University of Edinburgh (2004)"},{"key":"9162_CR48","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: A Collection of Examples Created with JGEX. In: http:\/\/woody.cs.wichita.edu\/collection\/index.html (2009)"},{"key":"9162_CR49","doi-asserted-by":"crossref","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane, part 2. Automated generation of visually dynamic presentations with the full-angle method and the deductive database method. J. Autom. Reason. (2009, in press)","DOI":"10.1007\/s10817-009-9163-4"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9162-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9162-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9162-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T21:48:16Z","timestamp":1739483296000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9162-5"}},"subtitle":["Part 1. Basic Features and the Manual Input Method"],"short-title":[],"issued":{"date-parts":[[2009,12,18]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["9162"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9162-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2009,12,18]]}}}