{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:02:53Z","timestamp":1760061773857},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,12,23]],"date-time":"2009-12-23T00:00:00Z","timestamp":1261526400000},"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-9163-4","type":"journal-article","created":{"date-parts":[[2009,12,22]],"date-time":"2009-12-22T00:37:27Z","timestamp":1261442247000},"page":"243-266","source":"Crossref","is-referenced-by-count":15,"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,23]]},"reference":[{"key":"9163_CR1","doi-asserted-by":"crossref","unstructured":"Ye, Z., Gao, X.S., Chou, S.C.: Visually dynamic presentation of proofs in plane geometry part 1. Basic features and the manual input method. J. Autom. Reason. (2009). doi: 10.1007\/s10817-009-9162-5","DOI":"10.1007\/s10817-009-9162-5"},{"key":"9163_CR2","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. Sci. Sin. 21, 159\u2013172 (1978); Automated theorem proving: after 25 years. Contemp. Math.-Am. Math. Soc. 29, 213\u2013234 (1984)","journal-title":"Sci. Sin."},{"key":"9163_CR3","doi-asserted-by":"crossref","unstructured":"Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger\u2019s algorithm. In: Proc. of SYMSAC\u201986, Waterloo, pp. 209\u2013214 (1986)","DOI":"10.1145\/32439.32480"},{"key":"9163_CR4","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":"9163_CR5","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert\u2019s Nullstellensatz. In: Proc. of SYMSAC\u201986, Waterloo, pp. 202\u2013208 (1986)","DOI":"10.1145\/32439.32479"},{"key":"9163_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages. 2nd GI Conference","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. 2nd GI Conference. Lecture Notes in Computer Science, vol. 33, pp. 134\u2013183. Springer, Berlin (1975)"},{"key":"9163_CR7","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/S0747-7171(88)80014-2","volume":"5","author":"D Arnon","year":"1988","unstructured":"Arnon, D., Mignotte, M.: On mechanical quantifier elimination for elementary algebra and geometry. J. Symb. Comput. 5, 237\u2013259 (1988)","journal-title":"J. Symb. Comput."},{"key":"9163_CR8","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"9163_CR9","volume-title":"Mechanical Geometry Theorem Proving","author":"SC Chou","year":"1988","unstructured":"Chou, S.C.: Mechanical Geometry Theorem Proving. D.Reidel, Dordrecht (1988)"},{"key":"9163_CR10","unstructured":"Wu, W.T.: Basic Principles of Mechanical Theorem Proving in Geometries. Press, Beijing (in Chinese) (1984). English Version. Springer, New York (1993)"},{"key":"9163_CR11","volume-title":"Modern Geometry","author":"CF Adler","year":"1958","unstructured":"Adler, C.F.: Modern Geometry. McGraw-Hill Book, Sydney (1958)"},{"key":"9163_CR12","unstructured":"Hilbert, D.: Foundations of Geometry, 1st edn. (in Germany) was published in 1899. Open Court, La Salla (1971)"},{"issue":"1","key":"9163_CR13","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":"3","key":"9163_CR14","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. Reason. 25(3), 219\u2013246 (2000)","journal-title":"J. Autom. Reason."},{"key":"9163_CR15","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":"9163_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-55602-8_153","volume-title":"Proceedings of CADE\u201311","author":"SC Chou","year":"1992","unstructured":"Chou, S.C., Gao, X.S.: Proving geometry statements of constructive type. In: Proceedings of CADE\u201311. Lecture Notes in Computer Science, vol. 607, pp. 20\u201334. Springer, New York (1992)"},{"key":"9163_CR17","unstructured":"Wilson, S., Fleuriot, J.D.: Combining dynamic geometry, automated geometry theorem proving, and diagrammatic proofs. In: Workshop on User Interfaces for Theorem Provers (UITP). http:\/\/www.dai.ed.ac.uk\/homes\/jdf\/entcs-geom-05.pdf (2005)"},{"key":"9163_CR18","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: A collection of 110 geometry theorems and machine produced proofs for them, TR-94-5. CS Dept., WSU (1994)"},{"key":"9163_CR19","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":"9163_CR20","unstructured":"Chou, S.C., Gao, X.S., Ye, Z.: A collection of GIF files created with JGEX. http:\/\/woody.cs.wichita.edu\/collection\/index.html (2009)"},{"key":"9163_CR21","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)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9163-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9163-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9163-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:49Z","timestamp":1559251309000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9163-4"}},"subtitle":["Part 2. Automated Generation of Visually Dynamic Presentations with the Full-Angle Method and the Deductive Database Method"],"short-title":[],"issued":{"date-parts":[[2009,12,23]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["9163"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9163-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,12,23]]}}}