Processing math: 100%
We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 21 Issue 5
September  2006
Turn off MathJax
Article Contents
Abstract
References
Wen-Tsun Wu, Xiao-Shan Gao. Automated Reasoning and Equation Solving with the Characteristic Set Method[J]. Journal of Computer Science and Technology, 2006, 21(5): 756-764.
Citation: Wen-Tsun Wu, Xiao-Shan Gao. Automated Reasoning and Equation Solving with the Characteristic Set Method[J]. Journal of Computer Science and Technology, 2006, 21(5): 756-764.
shu

Automated Reasoning and Equation Solving with the Characteristic Set Method

  • Key Laboratory of Mathematics Mechanization, Institute of Systems Science, AMSS, Chinese Academy of Sciences, Beijing 100080, P.R. China

More Information
  • Received Date: April 06, 2006
  • Revised Date: June 19, 2006
  • Published Date: September 14, 2006
    Abstract
  • A brief introduction to the characteristic set method is given forsolving algebraic equation systems and then the method is extended toalgebraic difference systems. The method can be used to decompose thezero set for a difference polynomial set in general form to the union ofdifference polynomial sets in triangular form. Based on thecharacteristic set method, a decision procedure for the first ordertheory over an algebraically closed field and a procedure to provecertain difference identities are proposed.
    • FullText(HTML)
    • References (34)
  • [1]
    Wu W T. On the decision problem and the mechanization of theorem-proving in elementary geometry. -\it Scientia Sinica}, 1978, (21): 159--172. Re-published in -\em Automated Theorem Proving: After 25 Years}, 1984, pp.213--234.
    [2]
    Chou S C. Mechanical Geometry Theorem Proving. Dordrecht: D.Reidel Publishing Company, 1988.
    [3]
    Chou S C, Gao X S, Zhang J Z. Machine Proofs in Geometry. Singapore: World Scientific, 1994.
    [4]
    Li H, Wu Y. Automated theorem proving in projective geometry with Cayley and bracket algebras. -\it Journal of Symbolic Computation}, 2004, (36): 717--762.
    [5]
    Kapur D, Mundy J L. Geometric reasoning. -\it Special Issue of Artificial Intelligence}, 1988, (37): 1--3.
    [6]
    Wu W T. Mathematics Mechanization. Beijing: Science Press/Kluwer, 2001.
    [7]
    Hsiang J. Herbrand award for Distinguished Contribution to Automated Reasoning. -\it Automated Deduction}, LNAI 1249, Springer, 1997, pp.4--7.
    [8]
    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.
    [9]
    Ritt J F. Differential Algebra. -\it Amer. Math. Soc. Colloquium}, Vol.33, Dover Publications, 1950.
    [10]
    Wu W T. Mechanical theorem proving in elementary differential geometry. -\it Scientia Sinica}, 1979, Math. Supplement: 94--102. (in Chinese)
    [11]
    Aubry P, Lazard D, Maza M M. On the theory of triangular sets. -\it Journal of Symbolic Computation}, 1999, (25): 105--124.
    [12]
    Bouziane D, Rody A Kandri, Ma\hat-\rm a}rouf H. Unmixed-dimensional decomposition of a finitely generated perfect differential ideal. -\it Journal of Symbolic Computation}, 2001, (31): 631--649.
    [13]
    Dahan X, Schost E. Sharp estimates for triangular sets. In -\it Proc. ISSAC2004}, New York, 2004, pp.103--110.
    [14]
    Gallo G, Mishra B. Efficient algorithms and bounds for Wu-Ritt characteristic sets. -\it Effective Methods in Algebraic Geometry, Progress in Mathematics}, 1991, (94): 119--142.
    [15]
    Gao X S, Chou S C. A zero structure theorem for differential parametric systems. -\it Journal of Symbolic Computation}, 1994, (16): 585--595.
    [16]
    Gao X S, Luo Y. A characteristic set method for difference polynomial systems. In -\it Int. Conf. Poly. Sys. Sol.}, Paris, Nov. 2004, pp.24--26. Submitted to JSC.
    [17]
    Hubert E. Factorization-free decomposition algorithms in differential algebra. -\it Journal of Symbolic Computation}, 2000, (29): 641--662.
    [18]
    Kalkbrener M. A generalized Euclidean algorithm for computing triangular representations of algebraic varieties. -\it Journal of Symbolic Computation}, 1993, (15): 143--167.
    [19]
    Wang D. Elimination Methods. Berlin: Springer, 2000.
    [20]
    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)
    [21]
    Gao X S, Hou X R, Tang J, Cheng H. Complete solution classification for the perspective-three-point problem. -\it IEEE Trans. PAMI}, 2003, 25(8): 930--943.
    [22]
    Kapur D, Mundy J L. Wu's method and its applications to perspective viewing. -\it Artificial Intelligence}, 1988, (37): 15--36.
    [23]
    Zhi L, Reid G, Tang J. A complete symbolic-numeric linear method for camera pose determination. In -\it Proc. ISSAC2003}, 2003, pp.215--223.
    [24]
    Gao X S, Lin Q, Zhang G. A C-tree decomposition algorithm for 2D and 3D geometric constraint solving. -\it Computer-Aided Design}, 2006, 38(1): 1--13.
    [25]
    Wu W T, Wang D K. On the surface fitting problems in CAGD. -\it Mathematics in Practice and Theory}, 1994, (3): 26--31. (in Chinese)
    [26]
    Mao W, Wu J. Application of Wu's method to symbolic model checking. In -\it Proc. ISSAC2005}, New York, 2005, pp.237--244.
    [27]
    He S, Zhang B. Solving SAT by algorithm transform of Wu's method. -\it J. Comput. Sci. and Technnol.}, 1999, 14(5): 468--480.
    [28]
    Gao X S, Lei D, Liao Q, Zhang G. Generalized Stewart-Gough platforms and their direct kinematics. -\it IEEE Trans. Robotics}, 2005, 21(2): 141--151.
    [29]
    Lu Z, He B, Luo Y. Real Roots Isolating for Polynomial Systems and Applications. Science Press, 2004.
    [30]
    Li Z, Schwarz F, Tsarev S. Factoring linear partial differential systems with finite-dimensional solution spaces. -\it Journal of Symbolic Computation}, 2003, (36): 443--471.
    [31]
    Wang S K, Wu K. Solving the Yang-Baxter equation by Wu's method. -\it Mathematics Mechanization and Applications}, San Diego: Academic Press, 2000, pp.95--121.
    [32]
    Wu W T. Basic principles of mechanical theorem proving in elementary geometries. -\it J. Sys. Sci. & Math. Scis.}, 1984, (4): 207--235. Re-published in -\it J. Automated Reasoning}, 1986, (2): 221--252.
    [33]
    Wu W T. Basic Principle of Mechanical Theorem Proving in Geometries. Beijing: Science Press, 1984; Wien: Springer, 1994. (in Chinese)
    [34]
    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.
    • Relative Articles
  • Supplements (0)

Catalog

    Get Citation
    XML
    Article views (14) PDF downloads (1832) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return