{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:11:44Z","timestamp":1762323104413,"version":"3.33.0"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sc. China"],"published-print":{"date-parts":[[2007,2]]},"DOI":"10.1007\/s11704-007-0001-8","type":"journal-article","created":{"date-parts":[[2007,3,20]],"date-time":"2007-03-20T00:16:29Z","timestamp":1174349789000},"page":"1-8","source":"Crossref","is-referenced-by-count":19,"title":["Mathematics mechanization and applications after thirty years"],"prefix":"10.1007","volume":"1","author":[{"given":"Wenjun","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoshan","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"P\u00f3lya G. Mathematical Discovery. Vol 1. John Wiley & Sons, 1962"},{"key":"1_CR2","volume-title":"Mathematics Machenization","author":"W. T. Wu","year":"2001","unstructured":"Wu W T. Mathematics Machenization. Beijing: Science Press\/Kluwer, 2001"},{"key":"1_CR3","doi-asserted-by":"crossref","DOI":"10.1090\/coll\/033","volume-title":"Differential Algebra","author":"J. F. Ritt","year":"1950","unstructured":"Ritt J F. Differential Algebra. New York: AMS Press, 1950"},{"key":"1_CR4","first-page":"207","volume":"4","author":"W. T. Wu","year":"1984","unstructured":"Wu W T. Basic principles of mechanical theorem-proving in elementary geometries. Sys Sci & Math Scis, 1984, 4: 207\u2013235; also in Journal of Automated Reasoning, 1986, 2: 221\u2013252","journal-title":"Sys Sci & Math Scis"},{"key":"1_CR5","volume-title":"Basic Principle of Mechanical Theorem Proving in Geometries","author":"W. T. Wu","year":"1984","unstructured":"Wu W T. Basic Principle of Mechanical Theorem Proving in Geometries. Beijing: Science Press, 1984 (in Chinese); English translation, Wien: Springer, 1994"},{"key":"1_CR6","first-page":"159","volume":"21","author":"W. T. Wu","year":"1978","unstructured":"Wu W T. On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica, 1978, 21: 159\u2013172","journal-title":"Scientia Sinica"},{"key":"1_CR7","volume-title":"Herbrand Award for Distinguished Constributions to Automated Reasoning, vi\u2013vii","author":"J. Hsiang","year":"1997","unstructured":"Hsiang J. Herbrand Award for Distinguished Constributions to Automated Reasoning, vi\u2013vii. Automated Deduction-CADE-14. LNAI 1249. Berlin: Springer, 1997"},{"key":"1_CR8","doi-asserted-by":"crossref","first-page":"930","DOI":"10.1109\/TPAMI.2003.1217599","volume":"25","author":"X. S. Gao","year":"2003","unstructured":"Gao X S, Hou X R, Tang J, et al. Complete solution classification for the perspective-three-point problem. IEEE Tran on PAMI, 2003, 25: 930\u2013943","journal-title":"IEEE Tran on PAMI"},{"key":"1_CR9","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0004-3702(88)90048-3","volume":"37","author":"D. Kapur","year":"1988","unstructured":"Kapur D, Mundy J L. Wu\u2019s method and its applications to perspective viewing. Artificial Intelligence, 1988, 37: 15\u201336","journal-title":"Artificial Intelligence"},{"key":"1_CR10","first-page":"211","volume":"1","author":"C. Su","year":"1997","unstructured":"Su C, Xu Y, Li H, et al. Application of Wu\u2019s method in computer animation. In: Proceedings of Fifth Int\u2019l Conf. CAD\/CG Vol 1. 1997, 211\u2013215","journal-title":"Proceedings of Fifth Int\u2019l Conf. CAD\/CG"},{"key":"1_CR11","first-page":"215","volume-title":"Proceedings of ISSAC\u201903","author":"L. Zhi","year":"2003","unstructured":"Zhi L, Reid G, Tang J. A complete symbolic-numeric linear method for camera pose determination. In: Proceedings of ISSAC\u201903. New York: ACM Press, 2003, 215\u2013223"},{"key":"1_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.cad.2005.03.002","volume":"38","author":"X. S. Gao","year":"2006","unstructured":"Gao X S, Lin Q, Zhang G. A C-tree decomposition algorithm for 2D and 3D geometric constraint solving. Computer-Aided Design, 2006, 38: 1\u201313","journal-title":"Computer-Aided Design"},{"key":"1_CR13","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1142\/9789812791962_0023","volume-title":"Computer Mathematics","author":"F. Chen","year":"2000","unstructured":"Chen F, Deng J, Feng Y. Algebraic surface blending using Wu\u2019s method. Computer Mathematics. Singapore: World Scientific, 2000, 172\u2013181"},{"key":"1_CR14","first-page":"383","volume":"17","author":"T. Wu","year":"2002","unstructured":"Wu T, Lei N, Cheng J. Wu Wen-tsun formulae for the blending of pipe surfaces. Northeast Math J, 2002, 17: 383\u2013386","journal-title":"Northeast Math J"},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1016\/0747-7171(92)90017-X","volume":"14","author":"X. S. Gao","year":"1992","unstructured":"Gao X S, Chou S C. Implicitization of rational parametric equations. Journal of Symbolic Computation, 1992, 14: 459\u2013470","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR16","first-page":"237","volume-title":"Proceedings of ISSAC\u201905","author":"W. Mao","year":"2005","unstructured":"Mao W, Wu J. Application of Wu\u2019s method to symbolic model checking. In: Proceedings of ISSAC\u201905. New York: ACM Press, 2005, 237\u2013244"},{"key":"1_CR17","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1109\/TRO.2004.835456","volume":"21","author":"X. S. Gao","year":"2005","unstructured":"Gao X S, Lei D, Liao Q, et al. Generalized Stewart-Gough platforms and their direct kinematics. IEEE Trans Robotics, 2005, 21: 141\u2013151","journal-title":"IEEE Trans Robotics"},{"key":"1_CR18","series-title":"LNCS","first-page":"207","volume-title":"Proceedings of CADE\u201910","author":"S. C. Chou","year":"1990","unstructured":"Chou S C, Gao X S. Ritt-Wu\u2019s decomposition algorithm and geometry theorem proving. In: Proceedings of CADE\u201910. LNCS, No 449. Berlin: Springer-Verlag, 1990, 207\u2013220"},{"key":"1_CR19","first-page":"101","volume-title":"Proceedings of ISSAC\u201906","author":"X. S. Gao","year":"2006","unstructured":"Gao X S, Yuan C. Resolvent systems of difference polynomial ideals. In: Proceedings of ISSAC\u201906. New York: ACM Press, 2006, 101\u2013108"},{"key":"1_CR20","unstructured":"Wu W T. Mechanical theorem proving inelementary differential geometry. Scientia Sinica, 1979, 94\u2013102 (in Chinese)"},{"key":"1_CR21","first-page":"158","volume-title":"Proceedings of ISSAC\u201995","author":"F. Boulier","year":"1995","unstructured":"Boulier F, Lazard D, Ollivier F, et al. Representation for the radical of a finitely generated differential ideal. In: Proceedings of ISSAC\u201995. New York: ACM Press, 1995, 158\u2013166."},{"key":"1_CR22","doi-asserted-by":"crossref","first-page":"631","DOI":"10.1006\/jsco.1999.1562","volume":"31","author":"D. Bouziane","year":"2001","unstructured":"Bouziane D, Kandri Rody A, Ma\u00e2rouf H. Unmixed decomposition of a finitely generated perfect differential ideal. Journal of Symbolic Computation, 2001, 31: 631\u2013649","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR23","first-page":"66","volume":"23","author":"X. S. Gao","year":"2004","unstructured":"Gao X S, Luo Y. A characteristic set method for difference polynomial systems. In: Inter Conf on Poly Sys Sol, Nov 24\u201326, Paris, 2004; also in MM-Preprints, 2004, 23: 66\u201391","journal-title":"Inter Conf on Poly Sys Sol, Nov 24\u201326, Paris, 2004"},{"key":"1_CR24","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1006\/jsco.1999.0269","volume":"25","author":"P. Aubry","year":"1999","unstructured":"Aubry P, Lazard D, Maza M M. On the theory of triangular sets. Journal of Symbolic Computation, 1999, 25: 105\u2013124","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR25","volume-title":"Elimination Methods","author":"D. Wang","year":"2000","unstructured":"Wang D. Elimination Methods. Berlin: Springer, 2000"},{"key":"1_CR26","first-page":"108","volume-title":"Proceedings of ISSAC\u201905","author":"X. Dahan","year":"2005","unstructured":"Dahan X, Maza M M, Schost E, et al. Lifting techniques for triangular decompositions. In: Proceedings of ISSAC\u201905. New York: ACM Press, 2005, 108\u2013115"},{"key":"1_CR27","first-page":"220","volume":"11","author":"W. T. Wu","year":"1990","unstructured":"Wu W T. On a projection theorem of quasi-varieties in elimination theory. Chinese Annals of Math B, 1990, 11: 220\u2013226","journal-title":"Chinese Annals of Math B"},{"key":"1_CR28","first-page":"119","volume-title":"Progress in Mathematics, 94","author":"G. Gallo","year":"1991","unstructured":"Gallo G, Mishra B. Efficient algorithms and bounds for Wu-Ritt characteristic sets. In: Progress in Mathematics, 94: Boston: Birkh\u00e4user, 1991, 119\u2013142"},{"key":"1_CR29","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1006\/jsco.1993.1011","volume":"15","author":"M. Kalkbrener","year":"1993","unstructured":"Kalkbrener M. A generalized Euclidean algorithm for computing triangular representations of algebraic varieties. Journal of Symbolic Computation, 1993, 15: 143\u2013167","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR30","volume-title":"Non-linear Algebraic Equations and Automated Theorem Proving","author":"L. Yang","year":"1996","unstructured":"Yang L, Zhang J Z, Hou X R. Non-linear Algebraic Equations and Automated Theorem Proving. Shanghai: ShangHai Science and Education Pub, 1996 (in Chinese)"},{"key":"1_CR31","doi-asserted-by":"crossref","first-page":"1260","DOI":"10.1360\/03ys0073","volume":"48","author":"F. Chen","year":"2005","unstructured":"Chen F, Yang W. Applications of interval arithmetic in solving polynomial equations by Wu\u2019s elimination method. Science in China, Ser A, 2005, 48: 1260\u20131273","journal-title":"Science in China, Ser A"},{"key":"1_CR32","first-page":"1","volume":"9","author":"W. T. Wu","year":"1993","unstructured":"Wu W T. On a hybrid method of polynomial equations solving. MM-Preprints, 1993, 9: 1\u201310","journal-title":"MM-Preprints"},{"key":"1_CR33","first-page":"277","volume-title":"Proceedings of ISSAC\u201990","author":"D. Kapur","year":"1990","unstructured":"Kapur D, Wan H K. Refutational proofs of geometry theorems via characteristic sets. In: Proceedings of ISSAC\u201990. New York: ACM Press, 1990, 277\u2013284"},{"key":"1_CR34","first-page":"97","volume":"7","author":"B. Li","year":"2005","unstructured":"Li B. An algorithem to decompose a polynomial ascending set into irredncible ones. Acta Anal Funct Appl, 2005, 7: 97\u2013105","journal-title":"Acta Anal Funct Appl"},{"issue":"2","key":"1_CR35","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1006\/jsco.1993.1035","volume":"16","author":"D. Wang","year":"1993","unstructured":"Wang D. An elimination method for polynomial systems. Journal of Symbolic Computation, 1993, 16(2): 83\u2013114","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR36","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF00881834","volume":"10","author":"S. C. Chou","year":"1993","unstructured":"Chou S C, Gao X S. Automated reasoning in differential geometry and mechanics. Journal of Automated Reasoning, 1993, 10: 161\u2013172","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR37","doi-asserted-by":"crossref","first-page":"641","DOI":"10.1006\/jsco.1999.0344","volume":"29","author":"E. Hubert","year":"2000","unstructured":"Hubert E. Factorization-free decomposition algorithms in differential algebra. Journal of Symbolic Computation, 2000, 29: 641\u2013662","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR38","first-page":"658","volume":"9","author":"D. Wang","year":"1995","unstructured":"Wang D. A method for proving theorems in differential geometry and mechanics. J Univ Comput Sci, 1995, 9: 658\u2013673","journal-title":"J Univ Comput Sci"},{"key":"1_CR39","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0747-7171(08)80122-8","volume":"12","author":"D. Richardson","year":"1991","unstructured":"Richardson D. Wu\u2019s method and the Khovanskii finiteness theorem. Journal of Symbolic Computation, 1991, 12: 127\u2013141","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR40","volume-title":"Equation Solvings and Theorem Provings-Problem Solvings with MMP","author":"X. S. Gao","year":"2006","unstructured":"Gao X S, Wang D K, Qiao Z, et al. Equation Solvings and Theorem Provings-Problem Solvings with MMP. Beijing: Science Press, 2006 (in Chinese)"},{"key":"1_CR41","unstructured":"Wang D K. Wsolve: A Maple Package for Solving System of Polynomial Equations. http:\/\/www.mmrc.iss.ac.cn\/dwang\/wsolve.htm . 2004"},{"key":"1_CR42","doi-asserted-by":"crossref","DOI":"10.1142\/9781848161207","volume-title":"Elimination Practice: Software Tools and Applications","author":"D. Wang","year":"2004","unstructured":"Wang D. Elimination Practice: Software Tools and Applications. London: Imperial College Press, 2004"},{"key":"1_CR43","volume-title":"Real Roots Isolating for Polynomial Systems and Applications","author":"Z. Lu","year":"2004","unstructured":"Lu Z, He B, Luo Y. Real Roots Isolating for Polynomial Systems and Applications. Beijing: Science Press, 2004 (in Chinese)."},{"key":"1_CR44","first-page":"289","volume":"2","author":"W. T. Wu","year":"1989","unstructured":"Wu W T. On the foundation of algebraic differential geometry. Sys Sci & Math Scis, 1989, 2: 289\u2013312","journal-title":"Sys Sci & Math Scis"},{"key":"1_CR45","first-page":"335","volume-title":"Proceedings of ISSAC\u201992","author":"X. S. Gao","year":"1992","unstructured":"Gao X S, Chou S C. Solving parametric algebraic systems. In: Proceedings of ISSAC\u201992. New York: ACM Press, 1992, 335\u2013341"},{"key":"1_CR46","first-page":"436","volume":"32","author":"W. T. Wu","year":"1986","unstructured":"Wu W T. A mechanization method of geometry and its applications, I. Distances, areas, and volumes in Euclidean and non-Euclidean Geometries. Kuxue Tongbao, 1986, 32: 436\u2013440","journal-title":"Kuxue Tongbao"},{"key":"1_CR47","volume-title":"Mechanical Geometry Theorem Proving","author":"S. C. Chou","year":"1988","unstructured":"Chou S C. Mechanical Geometry Theorem Proving. Dordrecht: D Reidel, 1988"},{"key":"1_CR48","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/BF01531322","volume":"13","author":"Z. Li","year":"1995","unstructured":"Li Z. Mechanical theorem proving of the local theory of surfaces. Ann Math Artif Intell, 1995, 13: 25\u201346","journal-title":"Ann Math Artif Intell"},{"key":"1_CR49","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":"1_CR50","first-page":"139","volume":"13","author":"J. Richter-Gebert","year":"1995","unstructured":"Richter-Gebert J. Mechanical theorem proving in projective geometry. Ann Math and Al, 1995, 13: 139\u2013172","journal-title":"Ann Math and Al"},{"key":"1_CR51","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005819428156","volume":"21","author":"H. Li","year":"1998","unstructured":"Li H, Cheng M. Clifford algebraic reduction method for mechanical theorem proving in differential geometry. Journal of Automated Reasoning, 1998, 21: 1\u201321","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR52","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1023\/A:1006182023017","volume":"25","author":"H. Li","year":"2000","unstructured":"Li H. Vectorial equation-solving for mechanical geometry theorem proving. Journal of Automated Reasoning, 2000, 25: 83\u2013121","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR53","first-page":"27","volume-title":"Geometric Computing with Clifford Algebra","author":"H. Li","year":"2000","unstructured":"Li H, Hestenes D, Rockwood A. Generalized homogeneous coordinates for computational geometry. Geometric Computing with Clifford Algebra. Berlin: Springer, 2000, 27\u201360"},{"key":"1_CR54","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1016\/S0747-7171(03)00067-1","volume":"36","author":"H. Li","year":"2004","unstructured":"Li H, Wu Y. Automated theorem proving in projective geometry with Cayley and bracket algebras. Journal of Symbolic Computation, 2004, 36: 717\u2013762","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Gerlentner H, Hanson J R, Loveland D W. Empirical explorations of the geometry-theorem proving machine. In: Proceedings of West Joint Computer Conf. 1960, 143\u2013147","DOI":"10.1145\/1460361.1460381"},{"key":"1_CR56","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"S. C. Chou","year":"2000","unstructured":"Chou S C, Gao X S, Zhang J Z. A deductive database approach to automated geometry theorem proving and discovering. Journal Automated Reasoning, 2000, 25: 219\u2013246","journal-title":"Journal Automated Reasoning"},{"key":"1_CR57","volume-title":"Geometry Expert","author":"X. S. Gao","year":"1998","unstructured":"Gao X S, Zhang J Z, Chou S C. Geometry Expert. Teipei: Nine Chapters Pub, 1998 (in Chinese)"},{"key":"1_CR58","series-title":"LNCS","first-page":"134","volume-title":"Quantifier elimination for real closed fields by cylindrical algebraic decomposition","author":"G. E. Collins","year":"1975","unstructured":"Collins G E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. LNCS, No 33. Berlin: Springer-Verlag, 1975, 134\u2013183"},{"key":"1_CR59","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1023\/A:1006031329384","volume":"21","author":"A. Dolzmann","year":"1998","unstructured":"Dolzmann A, Sturm T, Weispfenning V. A new approach for automatic theorem proving in real geometry. Journal of Automated Reasoning, 1998, 21: 357\u2013380","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR60","first-page":"193","volume":"7","author":"W. T. Wu","year":"1994","unstructured":"Wu W T. On a finiteness theorem about optimization problems. Sys Sci & Math Scis, 1994, 7: 193\u2013200","journal-title":"Sys Sci & Math Scis"},{"issue":"6","key":"1_CR61","first-page":"628","volume":"39","author":"L. Yang","year":"1996","unstructured":"Yang L, Hou X, Zeng Z. Complete discriminant systems. Science in China, Ser E, 1996, 39(6): 628\u2013646","journal-title":"Science in China, Ser E"},{"key":"1_CR62","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF02714567","volume":"44","author":"L. Yang","year":"2001","unstructured":"Yang L, Hou X, Xia B. A complete algorithm for automated discovering of a class of inequality-type theorems. Science in China, Ser F, 2001, 44: 33\u201349","journal-title":"Science in China, Ser F"},{"key":"1_CR63","unstructured":"Xu C, Shi Q, Cheng M. A global stereo vision method based on Wu-solver. In: Proceedings of GMICV\u201995. 1995, 198\u2013205"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-007-0001-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-007-0001-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-007-0001-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,15]],"date-time":"2025-01-15T03:48:45Z","timestamp":1736912925000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-007-0001-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":63,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2]]}},"alternative-id":["1"],"URL":"https:\/\/doi.org\/10.1007\/s11704-007-0001-8","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"type":"print","value":"1673-7350"},{"type":"electronic","value":"1673-7466"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}