The Characteristic Set Method
Developed from J. F. Ritt's work on differential algebra,
the Characteristic Set
Method was discovered independently by the Chinese
mathematician Wen-tsun
Wu in 1978. Hence the name Wu's Method.
Wu rediscovered the characteristic set method in
the context of his work on mechanical geometry theorem proving. He transferred
the algorithmic aspects of Ritt's method to ordinary polynomial rings with the
intent of finding an effective method for automating theorem proving in
elementary geometry.
Since then the method has proven to have a variety of applications.
Applications
The Characteristic Set Method has proven to have many applications. Dongming
Wang has given a survey on the applications of the Characteristic Set Method.
Interested reader is refered to references listed in the
following bibliography.
Here is a listing of some of the applications where the Characteristic Set
Method is applied.
- Mechanical Geometry Theorem Proving.
- Mechanical Derivation of Unknown Relations and Locus Equations.
- Solving Systems of Algebraic Equations.
- Polynomial Factorization and Decomposition.
- Constructive Algebraic Geometry.
- Discriminant Systems and Singularities of Algebraic Hypersurfaces.
- Implicitization of Parametric Objects.
- Definiteness of Polynomials and Proving Inequalities.
- Complex Root Isolation.
- Qualitative Problems of Differential Equations.
- Proving by Examples.
- Solving Transcendental Equations.
- Proving Khovanskii's Finiteness Theorem.
- Pole Assignment of Linear Control Systems.
Implementations
The Characteristic Sets Method has been implemented on most Computer Algebra
Systems including Mathematica, Maple, Macsyma, Axiom etc.
None commercial implementations include:
- CharSets: Version 2.0 for Maple V Release 3 is a package for
computing characteristic sets and zero decompositions by D. Wang.
You may get the package as
/pub/misc/charsets-2.0.tar.Z
- Wsolve: Version 1.0 for Maple V Release 2 is a
package for solving systems of polynomial equations by
D.K. Wang.
- SACCS : Version 1.0 for SACLIB is a package for computing
characteristic sets and zero decompositions by L.H.Zhi .
Bibliography
- Chou S.
Mechanical Geometry Theorem Proving
Reidel Publishing, 1988.
- Chou S. - Gao X.
Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving
Proceedings of the 10th International Conference on Automated Deduction
Lecture Notes in Computer Science, 449,
Springer-Verlag,
pp. 207-220, 1990.
- Cox D. - Little J. - O'Shea D.
Ideals, Varieties, and Algorithms. An Introduction to Computational
Algebraic Geometry and Commutative Algebra.
Springer-Verlag,
1991.
- Ritt J.
Differential Equations from the Algebraic Standpoint
American Mathematical Society, 1932.
- Ritt J.
Differential Algebra
American Mathematical Society, 1950.
- Wang D.
An Implementation of the Characteristic Set Method in Maple
RISC-Linz Series No. 91-25.0,
Johannes Kepler University, Austria, 1991.
.
- Wu, W. T.
On the Decision Problem and the Mechanization of
Theorem-Proving in Elementary Geometry
Sci. Sinica 21,
pp. 159-172, 1978.
(Also in: Automated Theorem Proving: after 25 years. Contemporary Mathematics, 29, pp. 213-234, 1984.)
- Wu, W. T.
Basic Principles of Mechanical Theorem Proving in Elementary Geometries
Journal of Sys. Sci. & Math. Scis. 4,
pp. 207-235, 1984.
(Also in: Journal of Automated Reasoning 2, pp. 221-252, 1986.)
Go Back to Zhi's Home