{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:02:10Z","timestamp":1760061730785},"reference-count":111,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Syst Sci Complex"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s11424-012-2048-3","type":"journal-article","created":{"date-parts":[[2012,8,9]],"date-time":"2012-08-09T09:51:22Z","timestamp":1344505882000},"page":"802-820","source":"Crossref","is-referenced-by-count":26,"title":["A review and prospect of readable machine proofs for geometry theorems"],"prefix":"10.1007","volume":"25","author":[{"given":"Jianguo","family":"Jiang","sequence":"first","affiliation":[]},{"given":"Jingzhong","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,8,10]]},"reference":[{"key":"2048_CR1","volume-title":"Foundations of Geometry","author":"D. Hilbert","year":"1971","unstructured":"D. Hilbert, Foundations of Geometry, Open Court Publishing Company, La Salla, Illinois, 1971."},{"key":"2048_CR2","volume-title":"Mathematics Mechanization","author":"W. T. Wu","year":"2003","unstructured":"W. T. Wu, Mathematics Mechanization, Science Press, Beijing, 2003."},{"key":"2048_CR3","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1948","unstructured":"A. Tarski, A Decision Method for Elementary Algebra and Geometry, The RAND Corporation Press, Santa Monica, 1948."},{"key":"2048_CR4","doi-asserted-by":"crossref","first-page":"365","DOI":"10.2307\/1969640","volume":"60","author":"A. Seidenberg","year":"1954","unstructured":"A. Seidenberg, A new decision method of elementary algebra, Annals of Mathematics, 1954, 60: 365\u2013371.","journal-title":"Annals of Mathematics"},{"key":"2048_CR5","volume-title":"Lecture Notes Computer Sciences 33","author":"G. Collins","year":"1975","unstructured":"G. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Lecture Notes Computer Sciences 33, Springer-Verlag, Berlin, Heidelberg, 1975."},{"key":"2048_CR6","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0004-3702(88)90049-5","volume":"37","author":"D. Arnon","year":"1988","unstructured":"D. Arnon, Geometric reasoning with logic and algebra, Artificial Intelligence, 1988, 37: 37\u201360.","journal-title":"Artificial Intelligence"},{"issue":"16","key":"2048_CR7","first-page":"157","volume":"21","author":"W. T. Wu","year":"1978","unstructured":"W. T. Wu, On the decision problem and the mechanization of theorem proving in elementary geometry, Journal of Systems Science and Mathematical Science, 1978, 21(16): 157\u2013179 (in Chinese).","journal-title":"Journal of Systems Science and Mathematical Science"},{"key":"2048_CR8","volume-title":"Basic Principles of Mechanical Theorem Proving in Geometries","author":"W. T. Wu","year":"1984","unstructured":"W. T. Wu, Basic Principles of Mechanical Theorem Proving in Geometries, Science Press, Beijing, 1984 (in Chinese)."},{"key":"2048_CR9","doi-asserted-by":"crossref","DOI":"10.1090\/coll\/033","volume-title":"Differential Algebra","author":"J. Ritt","year":"1950","unstructured":"J. Ritt, Differential Algebra, American Mathematical Society, New York, 1950."},{"key":"2048_CR10","first-page":"237","volume":"4","author":"S. C. Chou","year":"1988","unstructured":"S. C. Chou, An introduction to Wu\u2019s method for mechanical theorem proving in geometry, Journal of Automated Reasoning, 1988, 4: 237\u2013267.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR11","doi-asserted-by":"crossref","unstructured":"S. C. Chou, Proving Elementary Geometry Theorems Using Wu\u2019s Algorithm, Automated Theorem Proving: After 25 Years (ed. by W. Bledsoe and D. Loveland), AMS Contemporary Mathematics Series, 1984, 29: 243\u2013286.","DOI":"10.1090\/conm\/029\/14"},{"key":"2048_CR12","volume-title":"Mechanical Geometry Theorem Proving","author":"S. C. Chou","year":"1988","unstructured":"S. C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988."},{"key":"2048_CR13","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1016\/S0747-7171(86)80006-2","volume":"2","author":"B. Kutzler","year":"1986","unstructured":"B. Kutzler and S. Stifter, On the application of Buchberger\u2019s algorithm to automated geometry theorem proving, Journal of Symbolic Computation, 1986, 2: 389\u2013397.","journal-title":"Journal of Symbolic Computation"},{"issue":"19","key":"2048_CR14","first-page":"85","volume":"3","author":"B. Buchberger","year":"1995","unstructured":"B. Buchberger, G. Collins, and B. Kutzler, Algebraic methods for geometric reasoning, Annual Review of Computer Sciences, 1995, 3(19): 85\u2013119.","journal-title":"Annual Review of Computer Sciences"},{"key":"2048_CR15","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1145\/190347.190372","volume-title":"Proceedings of International Symposium on Symbolic and Algebraic Computation (Oxford, 1994)","author":"D. Kapur","year":"1994","unstructured":"D. Kapur, T. Saxena, and L. Yang, Algebraic and geometric reasoning with dixon resultants, Proceedings of International Symposium on Symbolic and Algebraic Computation (Oxford, 1994), ACM Press, New York, 1994 99\u2013107."},{"issue":"1","key":"2048_CR16","first-page":"10","volume":"15","author":"J. Z. Zhang","year":"1995","unstructured":"J. Z. Zhang, L. Yang, and X. R. Hou, The sub-resultant method for automated theorem proving, Journal of Systems Science and Mathematical Sciences, 1995, 15(1): 10\u201315. (in Chinese).","journal-title":"Journal of Systems Science and Mathematical Sciences"},{"key":"2048_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01531321","volume":"13","author":"D. M. Wang","year":"1995","unstructured":"D. M. Wang, Elimination procedures for mechanical theorem proving in geometry, Annals of Mathematics and Artificial Intelligence, 1995, 13: 1\u201324.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2048_CR18","first-page":"824","volume":"29","author":"J. W. Hong","year":"1986","unstructured":"J. W. Hong, Can geometry be proved by an example? Scientia Sinica, 1986, 29: 824\u2013834.","journal-title":"Scientia Sinica"},{"key":"2048_CR19","first-page":"34","volume":"1","author":"J. Z. Zhang","year":"1989","unstructured":"J. Z. Zhang and L. Yang, Principles of parallel numerical method and single-instance method of mechanical theorem proving, Mathematics in Practice and Theory, 1989, 1: 34\u201343.","journal-title":"Mathematics in Practice and Theory"},{"key":"2048_CR20","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(90)90077-U","volume":"74","author":"J. Z. Zhang","year":"1990","unstructured":"J. Z. Zhang, L. Yang, and M. Deng, The parallel numerical method of mechanical theorem proving, Theoretical Computer Science, 1990, 74: 253\u2013271.","journal-title":"Theoretical Computer Science"},{"key":"2048_CR21","doi-asserted-by":"crossref","unstructured":"H. Gelernter and N. Rochester, Intelligent behavior in problem-solving machines, IBM Journal, 1958: 336\u2013345.","DOI":"10.1147\/rd.24.0336"},{"key":"2048_CR22","volume-title":"Computers and Thought","author":"H. Gelernter","year":"1963","unstructured":"H. Gelernter, Realization of a Geometry Theorem Machine, Computers and Thought (ed. by E. Feigenbaum and J. Feldman), McGraw-Hill, New York, 1963."},{"key":"2048_CR23","volume-title":"Computers and Thought","author":"H. Gelernter","year":"1963","unstructured":"H. Gelernter, J. Hansen, and D. Loveland, Empirical Explorations of the Geometry Theorem Proving Machine, Computers and Thought (ed. by E. Feigenbaum and J. Feldman), McGraw-Hill, New York, 1963."},{"key":"2048_CR24","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, IV, A Collection of 400 Geometry Theorems, TR-92-7, Department of Computer Science, WSU, 1992."},{"key":"2048_CR25","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated production of traditional proofs for constructive geometry theorems, Proceedings of Eighth IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1993."},{"issue":"10","key":"2048_CR26","first-page":"721","volume":"19","author":"J. Z. Zhang","year":"1996","unstructured":"J. Z. Zhang, X. S. Gao, and S. C. Chou, The geometric information search system by forward reasoning, Chinese Journal of Computers, 1996, 19(10): 721\u2013727 (in Chinese).","journal-title":"Chinese Journal of Computers"},{"issue":"3","key":"2048_CR27","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"S. C. Chou","year":"2000","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, A deductive database approach to automated geometry theorem proving and discovering, Journal of Automated Reasoning, 2000, 25(3): 219\u2013246.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR28","volume-title":"Elementary Geometry Theorem Proving","author":"H. Goldstein","year":"1973","unstructured":"H. Goldstein, Elementary Geometry Theorem Proving, AIM-280, MIT, Cambridge, Massachusetts, 1973."},{"key":"2048_CR29","unstructured":"J. Anderson, C. Boyle, A. Corbett, and M. Lewis, The geometry tutor, Proceedings of IJCAI\u201985, Los Angles, 1985."},{"issue":"2","key":"2048_CR30","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/0004-3702(70)90005-6","volume":"1","author":"P. Gilmore","year":"1970","unstructured":"P. Gilmore, An examination of the geometry theorem proving machine, Artificial Intelligence, 1970, 1(2): 171\u2013187.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"2048_CR31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"A. Nevins","year":"1975","unstructured":"A. Nevins, Plane geometry theorem proving using forward chaining, Artificial Intelligence, 1975, 6(1): 1\u201323.","journal-title":"Artificial Intelligence"},{"key":"2048_CR32","volume-title":"Model-Driven Geometry Theorem Prover","author":"S. Ullman","year":"1975","unstructured":"S. Ullman, Model-Driven Geometry Theorem Prover, AIM-321, MIT, Cambridge, Massachusetts, 1975."},{"issue":"4","key":"2048_CR33","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H. Coelho","year":"1986","unstructured":"H. Coelho and L. Pereira, Automated reasoning in geometry theorem proving with prolog, Journal of Automated Reasoning, 1986, 2(4): 329\u2013390.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR34","volume-title":"Semantic Information Processing","author":"T. Evans","year":"1969","unstructured":"T. Evans, A Heuristic Program to Solve Geometry Analogy Problems, Semantic Information Processing (ed. by M. Minsky), MIT Press, Cambridge, 1969."},{"key":"2048_CR35","unstructured":"J. Anderson, Tuning of Search of the Problem Space for Geometry Proofs, Proceeding of IJCAI\u201981, Vancouver, 1981."},{"issue":"3","key":"2048_CR36","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/s10817-009-9163-4","volume":"45","author":"Y. Zheng","year":"2010","unstructured":"Y. Zheng, S. C. Chou, and X. S. Gao, Visually dynamic presentation of proofs in plane geometry \u2014 part 2. Automated generation of visually dynamic presentation with the Full-Angle method and the deductive database method, Journal of Automated Reasoning, 2010, 45(3): 243\u2013266","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR37","volume-title":"Geometry Expert","author":"X. S. Gao","year":"1998","unstructured":"X. S. Gao, J. Z. Zhang, and S. C. Chou, Geometry Expert, Nine Chapters Publishing, TaiPei, Taiwan, 1998 (in Chinese)."},{"issue":"5","key":"2048_CR38","first-page":"617","volume":"19","author":"J. G. Jiang","year":"2006","unstructured":"J. G. Jiang and J. Z. Zhang, The automated geometry reasoning network based on equivalent class reasoning, Patttern Recognition and Artificial Intelligence, 2006, 19(5): 617\u2013622 (in Chinese).","journal-title":"Patttern Recognition and Artificial Intelligence"},{"issue":"3","key":"2048_CR39","first-page":"135","volume":"38","author":"J. G. Jiang","year":"2006","unstructured":"J. G. Jiang and J. Z. Zhang, The automated geometry reasoning system based on RETE algorithm, Journal of Sichuan University: Engineering Science Edition, 2006, 38(3): 135\u2013139 (in Chinese).","journal-title":"Journal of Sichuan University: Engineering Science Edition"},{"issue":"2","key":"2048_CR40","doi-asserted-by":"crossref","first-page":"207","DOI":"10.3724\/SP.J.1016.2008.00207","volume":"31","author":"J. G. Jiang","year":"2008","unstructured":"J. G. Jiang, J. Z. Zhang, and X. J. Wang, Readable proving for a class of geometric theorems of polynomial equality type, Chinese Journal of Computers, 2008, 31(2): 207\u2013213 (in Chinese).","journal-title":"Chinese Journal of Computers"},{"key":"2048_CR41","unstructured":"R. Welham R, Geometry Problem Solving, D.A.I. Research Report No.14, 1976."},{"key":"2048_CR42","series-title":"Technical Memorandum","volume-title":"Construction Heuristics for Geometry and a Vector Algebra Representation of Geometry","author":"R. Wong","year":"1973","unstructured":"R. Wong, Construction Heuristics for Geometry and a Vector Algebra Representation of Geometry, Technical Memorandum 28, Project MAC, MIT, Cambridge, Massachusetts, 1973."},{"issue":"4","key":"2048_CR43","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/TC.1976.1674613","volume":"C-25","author":"R. Reiter","year":"1977","unstructured":"R. Reiter, A semantically guided deductive system for automatic theorem proving, IEEE Transactions on Computers, 1977, C-25(4): 328\u2013334.","journal-title":"IEEE Transactions on Computers"},{"key":"2048_CR44","volume-title":"Automation of Reasoning","author":"A. Robinson","year":"1983","unstructured":"A. Robinson, Proving a theorem (as done by Man, Logician, or Machine), Automation of Reasoning (ed. by J. Siekmann and G. Wrightson), Springer-Verlag, Berlin, Heidelberg, 1983."},{"key":"2048_CR45","unstructured":"W. Elcock, Representation of knowledge in geometry machine, Machine Intelligence (ed. by W. Elcock and D. Michie), John Wiley and Sons, 1977, 8: 11\u201329."},{"issue":"6","key":"2048_CR46","doi-asserted-by":"crossref","first-page":"445","DOI":"10.3758\/BF03198261","volume":"7","author":"G. Greeno","year":"1979","unstructured":"G. Greeno, M. Magone, and S. Chaiklin, Theory of constructions and set in problem solving, Memory and Cognition, 1979, 7(6): 445\u2013461.","journal-title":"Memory and Cognition"},{"issue":"1","key":"2048_CR47","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1023\/B:JARS.0000021960.39761.b7","volume":"32","author":"N. Matsuda","year":"2004","unstructured":"N. Matsuda and K. Van Lehn, GRAMY: A geometry theorem prover capable of construction, Journal of Automated Reasoning, 2004. 32(1): 3\u201333.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR48","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"J. McCharen, R. Overbeek, and L. Wos, Problems and experiments for and with automated theorem-proving programs, IEEE Transactions on Computers, 1976, C-25: 773\u2013782.","journal-title":"IEEE Transactions on Computers"},{"key":"2048_CR49","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF00245024","volume":"5","author":"A. Quaife","year":"1989","unstructured":"A. Quaife, Automated Development of Tarski\u2019s geometry, Journal of Automated Reasoning, 1989, 5: 97\u2013118.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR50","doi-asserted-by":"crossref","unstructured":"L. Meikle and J. Fleuriot, Formalizing Hilbert\u2019s grundlagen in Isabelle\/Isar, Theorem Proving in Higher Order Logics, 2003: 319\u2013334.","DOI":"10.1007\/10930755_21"},{"key":"2048_CR51","unstructured":"P. Scott, Mechanizing Hilbert\u2019s Foundations of Geometry in Isabelle, Master Thesis, School of Informatics, University of Edinburgh, 2008."},{"key":"2048_CR52","series-title":"LNAI","volume-title":"Automated Deduction in Geometry","author":"C. Dehlinger","year":"2001","unstructured":"C. Dehlinger, J. Dufourd, and P. Schreck, Higher-order intuitionistic formalization and proofs in Hilbert\u2019s elementary geometry, Automated Deduction in Geometry (2000), LNAI 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001."},{"key":"2048_CR53","doi-asserted-by":"crossref","unstructured":"J. Narboux, A decision procedure for geometry in Coq, Proceedings of TPHOLs\u2019 2004, LNCS 3223 (ed. by S. Konrad, B. Annett, and G. Genesh), 2004.","DOI":"10.1007\/978-3-540-30142-4_17"},{"key":"2048_CR54","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF01531326","volume":"13","author":"J. Z. Zhang","year":"1995","unstructured":"J. Z. Zhang, S. C. Chou, and X. S. Gao, Automated production of traditional proofs for theorems in Euclidean geometry, I: The Hilbert intersection point theorems, Annals of Mathematics and Artificial Intelligence, 1995, 13: 109\u2013137.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2048_CR55","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-007-9071-4","volume":"39","author":"J. Narboux","year":"2007","unstructured":"J. Narboux, A graphical user interface for formal proofs in geometry, Journal of Automated Reasoning, 2007, 39: 161\u2013180.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR56","series-title":"LNAI","volume-title":"Automated Deduction in Geometry (2000)","author":"R. Caferra","year":"2001","unstructured":"R. Caferra, N. Peltier, and F. Puitg, Emphasizing human techniques in automated geometry theorem proving: A practical realization, Automated Deduction in Geometry (2000), LNAI 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001."},{"key":"2048_CR57","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction in Geometry (1996)","author":"S. F\u00e8vre","year":"1998","unstructured":"S. F\u00e8vre, Integration of reasoning and algebraic calculus in geometry, Automated Deduction in Geometry (1996), Lecture Notes in Artificial Intelligence 1360, Springer-Verlag, Berlin, Heidelberg, 1998."},{"key":"2048_CR58","doi-asserted-by":"crossref","unstructured":"S. F`evre and D. M. Wang, Combining algebraic computing and term-rewriting for geometry theorem proving. Proceedings of AISC\u201998, Pittsburgh, USA, 1998.","DOI":"10.1007\/BFb0055909"},{"issue":"1\u20132","key":"2048_CR59","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1023\/A:1005944606876","volume":"20","author":"G. D\u00e9fourneaux","year":"1998","unstructured":"G. D\u00e9fourneaux, C. Bourely, and N. Peltier, Semantic generalizations for proving and disproving conjectures by analogy, Journal of Automated Reasoning, 1998, 20(1\u20132): 27\u201345.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR60","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems","author":"S. C. Chou","year":"1994","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems, World Scientific, Singapore, 1994."},{"key":"2048_CR61","volume-title":"Mathematics Mechanization and Applications","author":"J. Z. Zhang","year":"2000","unstructured":"J. Z. Zhang, Points Elimination Methods for Geometric Problem Solving, Mathematics Mechanization and Applications (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000."},{"issue":"4","key":"2048_CR62","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/s10817-010-9209-7","volume":"48","author":"P. Jani\u010di\u0107","year":"2012","unstructured":"P. Jani\u010di\u0107, J. Narboux, and P. Quaresma, The area method: A recapitulation, Journal of Automated Reasoning, 2012, 48(4): 489\u2013532","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR63","volume-title":"How to Solve Geometry Problems Using Areas","author":"J. Z. Zhang","year":"1982","unstructured":"J. Z. Zhang, How to Solve Geometry Problems Using Areas, Shanghai Educational Publishing Inc., Shanghai, 1982 (in Chinese)."},{"key":"2048_CR64","volume-title":"From Education of Mathematics to Mathematics for Education","author":"J. Z. Zhang","year":"1988","unstructured":"J. Z. Zhang and P. Cao, From Education of Mathematics to Mathematics for Education, Sichun Educational Publishing Inc., Chengdu, 1988 (in Chinese)."},{"key":"2048_CR65","volume-title":"A New Approach to Plane Geometry","author":"J. Z. Zhang","year":"1992","unstructured":"J. Z. Zhang, A New Approach to Plane Geometry, Sichuan Educational Publishing Inc., Chengdu, 1992 (in Chinese)."},{"issue":"3","key":"2048_CR66","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","volume":"17","author":"S. C. Chou","year":"1996","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated generation of readable proofs with geometric invariants, I: Multiple and shortest proofs generation, Journal of Automated Reasoning, 1996, 17(3): 325\u2013347.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"2048_CR67","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF00283134","volume":"17","author":"S. C. Chou","year":"1996","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated generation of readable proofs with geometric invariants, II: Theorem proving with full-angles, Journal of Automated Reasoning, 1996, 17(3): 349\u2013370.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR68","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, A Collection of 110 Geometry Theorems and Their Machine Proofs Based on Full-Angles, TR-94-4, Department of Computer Science, WSU, 1994."},{"key":"2048_CR69","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction in Geometry (2010)","author":"Y. Zou","year":"2011","unstructured":"Y. Zou and J. Z. Zhang, Automated generation of readable proofs for constructive geometry statements with the mass point method, Automated Deduction in Geometry (2010), Lecture Notes in Artificial Intelligence 6877, Springer-Verlag, Berlin Heidelberg, 2011."},{"key":"2048_CR70","volume-title":"Proceedings of International Symposium on Symbolic and Algebraic Computation","author":"S. C. Chou","year":"1993","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Mechanical geometry theorem proving by vector calculation, Proceedings of International Symposium on Symbolic and Algebraic Computation (Kiev, Ukraine, July 6\u20138, 1993), ACM Press, New York, 1993."},{"key":"2048_CR71","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BF00881858","volume":"14","author":"S. C. Chou","year":"1995","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated production of traditional proofs in solid geometry, Journal of Automated Reasoning, 1995, 14: 257\u2013291.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR72","series-title":"Lecture Notes Computer Sciences","volume-title":"Automated Deduction in Geometry","author":"L. Yang","year":"1997","unstructured":"L. Yang, X. S. Gao, S. C. Chou, and J. Z. Zhang, Automated production of readable proofs for theorems in non-euclidean geometries, Automated Deduction in Geometry, Lecture Notes Computer Sciences 1360, Springer-Verlag, Berlin, Heidelberg, 1997."},{"key":"2048_CR73","volume-title":"Mathematics Mechanization","author":"H. B. Li","year":"2000","unstructured":"H. B. Li, Clifford algebra approaches to mechanical geometry theorem proving, Mathematics Mechanization (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000."},{"key":"2048_CR74","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1016\/S0747-7171(08)80121-6","volume":"11","author":"B. Sturmfels","year":"1993","unstructured":"B. Sturmfels, Computational algebraic geometry of projective configurations, Journal of Symbolic Computation, 1993, 11: 595\u2013618.","journal-title":"Journal of Symbolic Computation"},{"key":"2048_CR75","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BF01531327","volume":"13","author":"J. Righter-Gebert","year":"1995","unstructured":"J. Righter-Gebert, Mechanical theorem proving in projective geometry, Annals of Mathematics and Artificial Intelligence, 1995, 13: 139\u2013172.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2048_CR76","volume-title":"New Explorations in Automated Theorem Proving in Geometries","author":"H. B. Li","year":"1994","unstructured":"H. B. Li, New Explorations in Automated Theorem Proving in Geometries, Ph.D. Thesis, Peking University, China, 1994."},{"key":"2048_CR77","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction in Geometry (1989)","author":"H. B. Li","year":"1998","unstructured":"H. B. Li, Some applications of clifford algebra to geometries, Automated Deduction in Geometry (1989), Lecture Notes in Artificial Intelligence 1669, Springer-Verlag, Berlin, Heidelberg, 1998."},{"key":"2048_CR78","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction in Geometry (1996)","author":"D. M. Wang","year":"1998","unstructured":"D. M. Wang, Clifford algebraic calculus for geometric reasoning with application to computer vision, Automated Deduction in Geometry (1996), Lecture Notes in Artificial Intelligence 1360, Springer-Verlag, Berlin, Heidelberg, 1998."},{"issue":"2","key":"2048_CR79","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BF02559961","volume":"13","author":"H. B. Li","year":"1997","unstructured":"H. B. Li and H. Shi, On Erd\u00f6s\u2019 ten-point problem, Acta Mathematica Sinica, New Series, 1997, 13(2): 221\u2013230.","journal-title":"Acta Mathematica Sinica, New Series"},{"key":"2048_CR80","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proving geometric theorems using clifford algebra and rewrite rules","author":"S. F\u00e8vre","year":"1997","unstructured":"S. F\u00e8vre and D. M. Wang, Proving geometric theorems using clifford algebra and rewrite rules, Lecture Notes in Artificial Intelligence 1421 (ed. by D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 1997."},{"key":"2048_CR81","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction in Geometry (Beijing, 1998)","author":"H. Q. Yang","year":"1999","unstructured":"H. Q. Yang, S. G. Zhang, and G. C. Feng, A Clifford algebraic method for geometric reasoning, Automated Deduction in Geometry (Beijing, 1998), Lecture Notes in Artificial Intelligence 1669 (ed. by X. S. Gao, D. M. Wang, and L. Yang), Springer-Verlag, Berlin, Heidelberg, 1999."},{"key":"2048_CR82","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1023\/A:1006182023017","volume":"25","author":"H. B. Li","year":"2000","unstructured":"H. B. Li, Vectorial equation-solving for mechanical geometry theorem proving, Journal of Automated Reasoning, 2000, 25: 83\u2013121.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR83","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005819428156","volume":"21","author":"H. B. Li","year":"1998","unstructured":"H. B. Li and M. Cheng, Clifford algebraic reduction method for automated theorem proving in differential geometries, Journal of Automated Reasoning, 1998, 21: 1\u201321.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR84","volume-title":"Mathematics Mechanization","author":"H. B. Li","year":"2000","unstructured":"H. B. Li, Mechanical theorem proving in differential geometry, Mathematics Mechanization (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000."},{"issue":"3","key":"2048_CR85","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1023\/A:1006031329384","volume":"21","author":"A. Dolzmann","year":"1998","unstructured":"A. Dolzmann, T. Sturm, and V. Weispfenning, A new approach for automatic theorem proving in real geometry, Journal of Automated Reasoning, 1998, 21(3): 357\u2013380.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR86","first-page":"103","volume":"7","author":"W. T. Wu","year":"1992","unstructured":"W. T. Wu, On problems involving inequalities, MM-Res, Preprints, MMRC, 1992, 7: 103\u2013138.","journal-title":"MM-Res, Preprints, MMRC"},{"issue":"2","key":"2048_CR87","first-page":"193","volume":"7","author":"W. T. Wu","year":"1994","unstructured":"W. T. Wu, On a finiteness theorem about problems involving inequalities, Journal of Systems Science and Mathematical Sciences, 1994, 7(2): 193\u2013200.","journal-title":"Journal of Systems Science and Mathematical Sciences"},{"key":"2048_CR88","volume-title":"Polynomial Equations Solving and Mechanical Geometric Theorem Proving","author":"D. M. Wang","year":"1993","unstructured":"D. M. Wang, Polynomial Equations Solving and Mechanical Geometric Theorem Proving, Ph.D. Thesis, Institute of Systems Science, Chinese Academy of Sciences, Beijing, 1993."},{"issue":"5","key":"2048_CR89","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/BF02948785","volume":"14","author":"L. Yang","year":"1999","unstructured":"L. Yang, Recent advances in automated theorem proving on inequalities, Journal of Computer Science and Technology, 1999, 14(5): 434\u2013446.","journal-title":"Journal of Computer Science and Technology"},{"issue":"1","key":"2048_CR90","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF02713938","volume":"44","author":"L. Yang","year":"2001","unstructured":"L. Yang, X. R. Hou, and B. C. Xia, A complete algorithm for automated discovering of a class of inequality-type theorems, Science in China (Series F), 2001, 44(1): 33\u201349.","journal-title":"Science in China (Series F)"},{"key":"2048_CR91","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction in Geometry","author":"L. Yang","year":"2001","unstructured":"L. Yang and J. Z. Zhang, A practical program of automated proving for a class of geometric inequalities, Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001."},{"key":"2048_CR92","volume-title":"Geometric Inequalities","author":"O. Bottema","year":"1969","unstructured":"O. Bottema, et al, Geometric Inequalities, Wolters-Noordhoff Publishing, Groningen, Netherlands, 1969."},{"key":"2048_CR93","volume-title":"Proceedings of the 10th Asian Technology Conference in Mathematics","author":"L. Yang","year":"2005","unstructured":"L. Yang, Solving harder problems with lesser mathematics, Proceedings of the 10th Asian Technology Conference in Mathematics, ATCM Inc., Blacksburg, 2005."},{"issue":"2","key":"2048_CR94","first-page":"1","volume":"5","author":"L. Yang","year":"2006","unstructured":"L. Yang, Difference substitution and automated inequality proving, Journal of Guangzhou University: Natural Science Edition, 2006, 5(2): 1\u20137 (in Chinese).","journal-title":"Journal of Guangzhou University: Natural Science Edition"},{"issue":"9","key":"2048_CR95","first-page":"1169","volume":"29","author":"L. Yang","year":"2009","unstructured":"L. Yang and Y. Yao, Difference substitution matrices and decision on nonnegativity of polynomials, Journal of Systems Science and Mathematical Sciences, 2009, 29(9): 1169\u20131177 (in Chinese).","journal-title":"Journal of Systems Science and Mathematical Sciences"},{"issue":"3","key":"2048_CR96","first-page":"251","volume":"53","author":"Y. Yao","year":"2010","unstructured":"Y. Yao, Infinite product convergence of column stochastic mean matrix and machine decision for positive semi-definite forms, Science China Mathematics (Series A), 2010, 53(3): 251\u2013264 (in Chinese).","journal-title":"Science China Mathematics (Series A)"},{"key":"2048_CR97","volume-title":"Automated Production of Readable Proof for a Class of Inequality-type Theorems","author":"S. H. Xia","year":"2002","unstructured":"S. H. Xia, Automated Production of Readable Proof for a Class of Inequality-type Theorems, Ph.D, Thesis, Chinese Academy of Sciences, Beijing, 2002."},{"issue":"4","key":"2048_CR98","first-page":"86","volume":"35","author":"S. Chen","year":"2003","unstructured":"S. Chen and J. Z. Zhang, Automated production of elementary and readable proof of inequality, Journal of Sichuan University: Engineering Science Education, 2003, 35(4): 86\u201393 (in Chinese).","journal-title":"Journal of Sichuan University: Engineering Science Education"},{"key":"2048_CR99","volume-title":"Proceedings of Asian Technology Conference in Mathematics","author":"S. C. Chou","year":"1995","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated geometry theorem proving and geometry education, Proceedings of Asian Technology Conference in Mathematics, Association of Mathematics Educators, Singapore, 1995."},{"key":"2048_CR100","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction in Geometry (1998)","author":"C. Z. Li","year":"1998","unstructured":"C. Z. Li and J. Z. Zhang, Readable machine solving in geometry and ICAI software MSG, Automated Deduction in Geometry (1998), Lecture Notes in Artificial Intelligence 1669, Springer-Verlag, Berlin, Heidelberg, 1998."},{"key":"2048_CR101","series-title":"Lecture Notes in Artifficial Intelligence","volume-title":"Proceedings of CADE-13","author":"S. C. Chou","year":"1996","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang, An introduction to geometry expert, Proceedings of CADE-13, Lecture Notes in Artifficial Intelligence (ed. by M. McRobbie and J. Slaney), Springer-Verlag, Berlin, Heidelberg, 1996."},{"key":"2048_CR102","unstructured":"Y. Zheng, S. C. Chou, and X. S. Gao, An introduction to java geometry expert-(extended abstract), Automated Deduction in Geometry \u2014 7th International Workshop (2008), LNCS 6301 (ed. by T. Sturm and C. Zengler), Springer, 2011."},{"issue":"3","key":"2048_CR103","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10817-009-9162-5","volume":"45","author":"Y. Zheng","year":"2010","unstructured":"Y. Zheng, S. C. Chou, and X. S. Gao, Visually dynamic presentation of proofs in plane geometry \u2014 part 1. Basic features and the manual input method, Journal of Automated Reasoning, 2010, 45(3): 213\u2013241.","journal-title":"Journal of Automated Reasoning"},{"key":"2048_CR104","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/978-3-540-24616-9_4","volume-title":"Automated Deduction in Geometry (Hagenberg Castle, Austria, 2002)","author":"X. S. Gao","year":"2004","unstructured":"X. S. Gao, Q. Lin, MMP\/Geometer-A software package for automated geometry reasoning, Automated Deduction in Geometry (Hagenberg Castle, Austria, 2002) (ed. by F. Winkler), Springer-Verlag, Berlin, Heidelberg, 2004: 44\u201366."},{"key":"2048_CR105","volume-title":"Super Sketchpad","author":"C. Z. Li","year":"2004","unstructured":"C. Z. Li and J. Z. Zhang, Super Sketchpad, Beijing Normal University Press, Beijing, 2004 (in Chinese)."},{"key":"2048_CR106","unstructured":"S. Wilson and J. Fleuriot, Geometry explorer: combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs, Proceedings of the 12th Workshop on Automated Reasoning (ARW), Edinburgh, UK, 2005."},{"key":"2048_CR107","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"International Joint Conference on Automated Reasoning (IJCAR-2006)","author":"P. Janicic","year":"2006","unstructured":"P. Janicic and P. Quaresma, System description: GCLCprover + GeoThms, International Joint Conference on Automated Reasoning (IJCAR-2006), Lecture Notes in Artificial Intelligence 4130 (ed. by U. Furbach and N. Shankar), Springer-Verlag, Berlin, Heidelberg, 2006."},{"issue":"8","key":"2048_CR108","first-page":"2101","volume":"31","author":"H. Zheng","year":"2011","unstructured":"H. Zheng and J. Z. Zhang, Reasoning of algorithm of geometry automatic reasoning platform with sustainable development by user, Journal of Computer Applications, 2011, 31(8): 2101\u20132107 (in Chinese).","journal-title":"Journal of Computer Applications"},{"issue":"12","key":"2048_CR109","first-page":"1622","volume":"31","author":"H. Zheng","year":"2011","unstructured":"H. Zheng, The sustainable geometry automated reasoning platform, Journal of System Science and Mathematical Sciences, 2011, 31(12): 1622\u20131632 (in Chinese).","journal-title":"Journal of System Science and Mathematical Sciences"},{"issue":"3","key":"2048_CR110","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1147\/rd.33.0210","volume":"3","author":"A. Samuel","year":"1959","unstructured":"A. Samuel, Some studies in machine learning using the game of checkers, IBM Journal of Research and Development, 1959, 3(3): 210\u2013229.","journal-title":"IBM Journal of Research and Development"},{"issue":"6","key":"2048_CR111","doi-asserted-by":"crossref","first-page":"601","DOI":"10.1147\/rd.116.0601","volume":"11","author":"A. Samuel","year":"1967","unstructured":"A. Samuel, Some studies in machine learning using the game of checkers II \u2014 Recent progress, IBM Journal of Research and Development, 1967, 11(6): 601\u2013617.","journal-title":"IBM Journal of Research and Development"}],"container-title":["Journal of Systems Science and Complexity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-012-2048-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11424-012-2048-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-012-2048-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T17:37:54Z","timestamp":1562089074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11424-012-2048-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":111,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["2048"],"URL":"https:\/\/doi.org\/10.1007\/s11424-012-2048-3","relation":{},"ISSN":["1009-6124","1559-7067"],"issn-type":[{"value":"1009-6124","type":"print"},{"value":"1559-7067","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8]]}}}