{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,17]],"date-time":"2025-04-17T15:27:24Z","timestamp":1744903644373},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2006,9,1]],"date-time":"2006-09-01T00:00:00Z","timestamp":1157068800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2006,9]]},"DOI":"10.1007\/s11390-006-0756-7","type":"journal-article","created":{"date-parts":[[2006,10,15]],"date-time":"2006-10-15T10:38:59Z","timestamp":1160908739000},"page":"756-764","source":"Crossref","is-referenced-by-count":6,"title":["Automated Reasoning and Equation Solving with the Characteristic Set Method"],"prefix":"10.1007","volume":"21","author":[{"given":"Wen-Tsun","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"756_CR1","unstructured":"Wu W T. On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica, 1978, (21): 159\u2013172. Re-published in Automated Theorem Proving: After 25 Years, 1984, pp. 213\u2013234."},{"key":"756_CR2","volume-title":"Mechanical Geometry Theorem Proving","author":"S C Chou","year":"1988","unstructured":"Chou S C. Mechanical Geometry Theorem Proving. Dordrecht: D.Reidel Publishing Company, 1988."},{"key":"756_CR3","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":"756_CR4","doi-asserted-by":"crossref","unstructured":"Li H, Wu Y. Automated theorem proving in projective geometry with Cayley and bracket algebras. Journal of Symbolic Computation, 2004, (36): 717\u2013762.","DOI":"10.1016\/S0747-7171(03)00067-1"},{"key":"756_CR5","doi-asserted-by":"crossref","unstructured":"Kapur D, Mundy J L. Geometric reasoning. Special Issue of Artificial Intelligence, 1988, (37): 1\u20133.","DOI":"10.1016\/0004-3702(88)90047-1"},{"key":"756_CR6","volume-title":"Mathematics Mechanization","author":"W T Wu","year":"2001","unstructured":"Wu W T. Mathematics Mechanization. Beijing: Science Press\/Kluwer, 2001."},{"key":"756_CR7","unstructured":"Hsiang J. Herbrand award for Distinguished Contribution to Automated Reasoning. Automated Deduction, LNAI 1249, Springer, 1997, pp. 4\u20137."},{"key":"756_CR8","doi-asserted-by":"crossref","unstructured":"Chou S C, Gao X S. Automated Reasoning in Geometry. Handbook of Automated Reasoning, Robinson A, Voronkov A (eds.), Amsterdam: Elsevier, 2001, pp. 709\u2013749.","DOI":"10.1016\/B978-044450813-3\/50013-8"},{"key":"756_CR9","doi-asserted-by":"crossref","unstructured":"Ritt J F. Differential Algebra. Amer. Math. Soc. Colloquium, Vol.33, Dover Publications, 1950.","DOI":"10.1090\/coll\/033"},{"key":"756_CR10","unstructured":"Wu W T. Mechanical theorem proving in elementary differential geometry. Scientia Sinica, 1979, Math. Supplement: 94\u2013102. (in Chinese)"},{"key":"756_CR11","doi-asserted-by":"crossref","unstructured":"Aubry P, Lazard D, Maza M M. On the theory of triangular sets. Journal of Symbolic Computation, 1999, (25): 105\u2013124.","DOI":"10.1006\/jsco.1999.0269"},{"key":"756_CR12","doi-asserted-by":"crossref","unstructured":"Bouziane D, Rody A Kandri, Ma\u00e2rouf H. Unmixed-dimensional decomposition of a finitely generated perfect differential ideal. Journal of Symbolic Computation, 2001, (31): 631\u2013649.","DOI":"10.1006\/jsco.1999.1562"},{"key":"756_CR13","doi-asserted-by":"crossref","unstructured":"Dahan X, Schost E. Sharp estimates for triangular sets. In Proc. ISSAC2004, New York, 2004, pp. 103\u2013110.","DOI":"10.1145\/1005285.1005302"},{"key":"756_CR14","doi-asserted-by":"crossref","unstructured":"Gallo G, Mishra B. Efficient algorithms and bounds for Wu-Ritt characteristic sets. Effective Methods in Algebraic Geometry, Progress in Mathematics, 1991, (94): 119\u2013142.","DOI":"10.1007\/978-1-4612-0441-1_8"},{"key":"756_CR15","doi-asserted-by":"crossref","unstructured":"Gao X S, Chou S C. A zero structure theorem for differential parametric systems. Journal of Symbolic Computation, 1994, (16): 585\u2013595.","DOI":"10.1006\/jsco.1993.1065"},{"key":"756_CR16","unstructured":"Gao X S, Luo Y. A characteristic set method for difference polynomial systems. In Int. Conf. Poly. Sys. Sol., Paris, Nov. 2004, pp. 24\u201326. Submitted to JSC."},{"key":"756_CR17","doi-asserted-by":"crossref","unstructured":"Hubert E. Factorization-free decomposition algorithms in differential algebra. Journal of Symbolic Computation, 2000, (29): 641\u2013662.","DOI":"10.1006\/jsco.1999.0344"},{"key":"756_CR18","doi-asserted-by":"crossref","unstructured":"Kalkbrener M. A generalized Euclidean algorithm for computing triangular representations of algebraic varieties. Journal of Symbolic Computation, 1993, (15): 143\u2013167.","DOI":"10.1006\/jsco.1993.1011"},{"key":"756_CR19","volume-title":"Elimination Methods","author":"D Wang","year":"2000","unstructured":"Wang D. Elimination Methods. Berlin: Springer, 2000."},{"key":"756_CR20","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)"},{"issue":"8","key":"756_CR21","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, Cheng H. Complete solution classification for the perspective-three-point problem. IEEE Trans. PAMI, 2003, 25(8): 930\u2013943.","journal-title":"IEEE Trans. PAMI"},{"key":"756_CR22","doi-asserted-by":"crossref","unstructured":"Kapur D, Mundy J L. Wu\u2019s method and its applications to perspective viewing. Artificial Intelligence, 1988, (37): 15\u201336.","DOI":"10.1016\/0004-3702(88)90048-3"},{"key":"756_CR23","doi-asserted-by":"crossref","unstructured":"Zhi L, Reid G, Tang J. A complete symbolic-numeric linear method for camera pose determination. In Proc. ISSAC2003, 2003, pp. 215\u2013223.","DOI":"10.1145\/860854.860900"},{"issue":"1","key":"756_CR24","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): 1\u201313.","journal-title":"Computer-Aided Design"},{"key":"756_CR25","unstructured":"Wu W T, Wang D K. On the surface fitting problems in CAGD. Mathematics in Practice and Theory, 1994, (3): 26\u201331. (in Chinese)"},{"key":"756_CR26","doi-asserted-by":"crossref","unstructured":"Mao W, Wu J. Application of Wu\u2019s method to symbolic model checking. In Proc. ISSAC2005, New York, 2005, pp. 237\u2013244.","DOI":"10.1145\/1073884.1073918"},{"issue":"5","key":"756_CR27","doi-asserted-by":"crossref","first-page":"468","DOI":"10.1007\/BF02948788","volume":"14","author":"S He","year":"1999","unstructured":"He S, Zhang B. Solving SAT by algorithm transform of Wu\u2019s method. J. Comput. Sci. and Technnol., 1999, 14(5): 468\u2013480.","journal-title":"J. Comput. Sci. and Technnol."},{"issue":"2","key":"756_CR28","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, Zhang G. Generalized Stewart-Gough platforms and their direct kinematics. IEEE Trans. Robotics, 2005, 21(2): 141\u2013151.","journal-title":"IEEE Trans. Robotics"},{"key":"756_CR29","unstructured":"Lu Z, He B, Luo Y. Real Roots Isolating for Polynomial Systems and Applications. Science Press, 2004."},{"key":"756_CR30","doi-asserted-by":"crossref","unstructured":"Li Z, Schwarz F, Tsarev S. Factoring linear partial differential systems with finite-dimensional solution spaces. Journal of Symbolic Computation, 2003, (36): 443\u2013471.","DOI":"10.1016\/S0747-7171(03)00090-7"},{"key":"756_CR31","doi-asserted-by":"crossref","unstructured":"Wang S K, Wu K. Solving the Yang-Baxter equation by Wu\u2019s method. Mathematics Mechanization and Applications, San Diego: Academic Press, 2000, pp. 95\u2013121.","DOI":"10.1016\/B978-012734760-8\/50005-3"},{"key":"756_CR32","doi-asserted-by":"crossref","unstructured":"Wu W T. Basic principles of mechanical theorem proving in elementary geometries. J. Sys. Sci. & Math. Scis., 1984, (4): 207\u2013235. Re-published in J. Automated Reasoning, 1986, (2): 221\u2013252.","DOI":"10.1007\/BF02328447"},{"key":"756_CR33","doi-asserted-by":"crossref","unstructured":"Wu W T. Basic Principle of Mechanical Theorem Proving in Geometries. Beijing: Science Press, 1984; Wien: Springer, 1994. (in Chinese)","DOI":"10.1007\/978-3-7091-6639-0"},{"key":"756_CR34","first-page":"130","volume-title":"Zero Decomposition Tree for Counting the Number of Solutions for Algebraic Parametric Equation Systems. Computer Mathematics III","author":"X S Gao","year":"2003","unstructured":"Gao X S, Wang D K. Zero Decomposition Tree for Counting the Number of Solutions for Algebraic Parametric Equation Systems. Computer Mathematics III, Singapore: World Scientific, 2003, pp. 130\u2013145."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0756-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-006-0756-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0756-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T14:32:37Z","timestamp":1559399557000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-006-0756-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9]]},"references-count":34,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["756"],"URL":"https:\/\/doi.org\/10.1007\/s11390-006-0756-7","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,9]]}}}