Abstract
This is the first paper of a series of three papers under the same title. It presents an improved version of Ritt-Wu's decomposition algorithm which is the basis of our methods of mechanical theorem proving and mechanical formula derivation in differential geometry and elementary mechanics. We improve the original algorithm in two aspects. First, by using the weak ascending chain and W-perm, the sizes of the differential polynomials occurring in the decomposition can be reduced. Second, by using a special reduction procedure, the number of branches in the decomposition can be controlled effectively. The improved version significantly enhances the efficiency of the original algorithm.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Blum, L., ‘Differentially closed fields: A model-theoretic tour’, in:Contributions to Algebra (Eds. H. Basset al.), Academic Press, New York, pp. 37–62 (1977).
Chou, S. C.,Mechanical Geometry Theorem Proving, D. Reidel Publishing Company (1988).
Chou, S. C. and Gao, X. S., ‘Mechanical theorem proving in differential geometry, I. Space curves’, TR-89-08, Computer Sciences Department, The University of Texas at Austin (March 1989).
Chou, S. C. and Gao, X. S., ‘Automated reasoning in mechanics using Ritt-Wu's method‘, TR-89-11, Computer Sciences Department, The University of Texas at Austin (April 1989).
Chou, S. C. and Gao, X. S., Ritt-Wu's decomposition algorithm and geometry theorem proving’, TR-89-09, Computer Sciences Department, The University of Texas at Austin (March 1989).
Chou, S. C. and Schelter, W. F., ‘Proving geometry theorem with rewrite rules’,J. Automated Reasoning 2(4), 253–273 (1986).
Kapur, D., ‘Geometry theorem proving using Hilbert's nullstellensatz’,Proc. SYMSAC'86, Waterloo, pp. 202–208 (1986).
Kutzler, B. and Stifter, S., ‘Automated geometry theorem proving using Buchberger's algorithm’,Proc. SYMSAC'86, Waterloo, pp. 209–214 (1986).
Ritt, J. F., ‘Differential equations from the algebraic standpoint’,Amer. Math. Soc. Colloquium,14, (1932).
Ritt, J. F., ‘Differential algebra’,Amer. Math. Soc. Colloquium (1950).
van der Waerden,Mathematische Annalen 96, 189 (1927).
Wang, D. M. and Gao, X. S., ‘Geometry theorems proved mechanically using Wu's method, Part on elementary geometries’, MM preprint No. 2 (1987).
Wu Wen-Tsün, ‘On the decision problem and the mechanization of theorem in elementary geometry’,Scientia Sinica 21, 159–172 (1978); Republished inAutomated Theorem Proving: After 25 Years, American Mathematics Society, Contemporary Mathematics,29, 213–234 (1984).
Wu Wen-Tsün, ‘Mechanical theorem proving in elementary differential geometry’,Scientia Sinica, Mathematics Supplement (I), 94–102 (1979). (In Chinese.)
Wu Wen-Tsün, ‘Mechanical theorem proving in elementary geometry and differential geometry’,Proc. 1980 Beijing, DD1 Symp. Vol. 2, Science Press, pp. 1073–1092 (1982).
Wu Wen-Tsün, ‘A constructive theory of differential algebraic geometry’,Lect. Notes in Math., No. 1255, pp. 173–189, Springer-Verlag (1987).
Author information
Authors and Affiliations
Additional information
The work reported here was supported in part by NSF Grants CCR-8702108 and CCR-9117870.
Rights and permissions
About this article
Cite this article
Chou, SC., Gao, XS. Automated reasoning in differential geometry and mechanics using the characteristic set method. J Autom Reasoning 10, 161–172 (1993). https://doi.org/10.1007/BF00881834
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF00881834