Abstract
A brief introduction to the characteristic set method is given for solving algebraic equation systems and then the method is extended to algebraic difference systems. The method can be used to decompose the zero set for a difference polynomial set in general form to the union of difference polynomial sets in triangular form. Based on the characteristic set method, a decision procedure for the first order theory over an algebraically closed field and a procedure to prove certain difference identities are proposed.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Wu W T. On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica, 1978, (21): 159–172. Re-published in Automated Theorem Proving: After 25 Years, 1984, pp. 213–234.
Chou S C. Mechanical Geometry Theorem Proving. Dordrecht: D.Reidel Publishing Company, 1988.
Chou S C, Gao X S, Zhang J Z. Machine Proofs in Geometry. Singapore: World Scientific, 1994.
Li H, Wu Y. Automated theorem proving in projective geometry with Cayley and bracket algebras. Journal of Symbolic Computation, 2004, (36): 717–762.
Kapur D, Mundy J L. Geometric reasoning. Special Issue of Artificial Intelligence, 1988, (37): 1–3.
Wu W T. Mathematics Mechanization. Beijing: Science Press/Kluwer, 2001.
Hsiang J. Herbrand award for Distinguished Contribution to Automated Reasoning. Automated Deduction, LNAI 1249, Springer, 1997, pp. 4–7.
Chou S C, Gao X S. Automated Reasoning in Geometry. Handbook of Automated Reasoning, Robinson A, Voronkov A (eds.), Amsterdam: Elsevier, 2001, pp. 709–749.
Ritt J F. Differential Algebra. Amer. Math. Soc. Colloquium, Vol.33, Dover Publications, 1950.
Wu W T. Mechanical theorem proving in elementary differential geometry. Scientia Sinica, 1979, Math. Supplement: 94–102. (in Chinese)
Aubry P, Lazard D, Maza M M. On the theory of triangular sets. Journal of Symbolic Computation, 1999, (25): 105–124.
Bouziane D, Rody A Kandri, Maârouf H. Unmixed-dimensional decomposition of a finitely generated perfect differential ideal. Journal of Symbolic Computation, 2001, (31): 631–649.
Dahan X, Schost E. Sharp estimates for triangular sets. In Proc. ISSAC2004, New York, 2004, pp. 103–110.
Gallo G, Mishra B. Efficient algorithms and bounds for Wu-Ritt characteristic sets. Effective Methods in Algebraic Geometry, Progress in Mathematics, 1991, (94): 119–142.
Gao X S, Chou S C. A zero structure theorem for differential parametric systems. Journal of Symbolic Computation, 1994, (16): 585–595.
Gao X S, Luo Y. A characteristic set method for difference polynomial systems. In Int. Conf. Poly. Sys. Sol., Paris, Nov. 2004, pp. 24–26. Submitted to JSC.
Hubert E. Factorization-free decomposition algorithms in differential algebra. Journal of Symbolic Computation, 2000, (29): 641–662.
Kalkbrener M. A generalized Euclidean algorithm for computing triangular representations of algebraic varieties. Journal of Symbolic Computation, 1993, (15): 143–167.
Wang D. Elimination Methods. Berlin: Springer, 2000.
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)
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–943.
Kapur D, Mundy J L. Wu’s method and its applications to perspective viewing. Artificial Intelligence, 1988, (37): 15–36.
Zhi L, Reid G, Tang J. A complete symbolic-numeric linear method for camera pose determination. In Proc. ISSAC2003, 2003, pp. 215–223.
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–13.
Wu W T, Wang D K. On the surface fitting problems in CAGD. Mathematics in Practice and Theory, 1994, (3): 26–31. (in Chinese)
Mao W, Wu J. Application of Wu’s method to symbolic model checking. In Proc. ISSAC2005, New York, 2005, pp. 237–244.
He S, Zhang B. Solving SAT by algorithm transform of Wu’s method. J. Comput. Sci. and Technnol., 1999, 14(5): 468–480.
Gao X S, Lei D, Liao Q, Zhang G. Generalized Stewart-Gough platforms and their direct kinematics. IEEE Trans. Robotics, 2005, 21(2): 141–151.
Lu Z, He B, Luo Y. Real Roots Isolating for Polynomial Systems and Applications. Science Press, 2004.
Li Z, Schwarz F, Tsarev S. Factoring linear partial differential systems with finite-dimensional solution spaces. Journal of Symbolic Computation, 2003, (36): 443–471.
Wang S K, Wu K. Solving the Yang-Baxter equation by Wu’s method. Mathematics Mechanization and Applications, San Diego: Academic Press, 2000, pp. 95–121.
Wu W T. Basic principles of mechanical theorem proving in elementary geometries. J. Sys. Sci. & Math. Scis., 1984, (4): 207–235. Re-published in J. Automated Reasoning, 1986, (2): 221–252.
Wu W T. Basic Principle of Mechanical Theorem Proving in Geometries. Beijing: Science Press, 1984; Wien: Springer, 1994. (in Chinese)
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–145.
Author information
Authors and Affiliations
Corresponding author
Additional information
Regular Paper: This work is supported by the National Grand Fundamental Research 973 Program of China under Grant No. 2004CB318000.
Wen-Tsun Wu is a professor at the Academy of Mathematics and Systems Sciences, Chinese Academy of Sciences and a member of Chinese Academy of Sciences. In the 1950s, Wu discovered the Wu class and Wu formulas in topology. In the late 1970s, Prof. Wu invented a method of automated geometry theorem proving, known as Wu’s method, and a method of solving algebraic and differential equations, known as Ritt-Wu’s zero decomposition theorem. He was a recipient of the Herbrand Award for Distinguished Contributions to Automated Reasoning in 1997, the National Supreme Award of Science and Technology of China in 2000, and the Shaw Prize in Mathematical Sciences 2006.
Xiao-Shan Gao is a professor and the director of the Institute of Systems Science, Chinese Academy of Sciences. His research interests include: automated reasoning, symbolic computation, intelligent CAD, CAGD, and robotics. He has published over one hundred research papers. Webpage: http://www.mmrc.iss.ac.cn/∼xgao.
Rights and permissions
About this article
Cite this article
Wu, WT., Gao, XS. Automated Reasoning and Equation Solving with the Characteristic Set Method. J Comput Sci Technol 21, 756–764 (2006). https://doi.org/10.1007/s11390-006-0756-7
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/s11390-006-0756-7