Abstract
In this paper, we present an algorithm to compute the projection of a quasi variety over an algebraic closed field. Based on the algorithm, we give a method to prove geometric theorem mechanically, and the non-degenerate conditions that we get by the method are proved to be the ”weakest”, i.e. the geometric theorem is true if and only if these non-degenerate conditions are satisfied. A method for automatic geometric formula deduction is also proposed based on the algorithm. The algorithm given in this paper has been implemented in computer algebra system Maple.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Wen-tsun, W.: Basic Principles of Mechanical Theorem Proving in Elementary Geometries. J. Sys. Sci. & Math. Scis. 4, 207–235 (1984)
Chou, S.-C.: Mechanical geometry theorem proving. D. Reidel, Dordrecht (1988)
Kapur, D.: Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation 2(4), 399–408 (1986)
Kutzler, B., Stifter, S.: On the application of Buchberger’s algorithm to automatic Geometry theorem Proving. Journal of Symbolic Computation 2(4), 389–397 (1986)
Chou, S.C., Schelter, W.F.: Automated Geometry Theorem Proving Using Rewrite Rules. Dept. of Mathematics. University of Texas, Austin (1985)
Winkler, F.: Automated Theorem Proving in Nonlinear Geometry. Advances in Computing Research 6, 138–197 (1992)
Wen-tsun, W.: On a Projection Theorem of Quasi-Varieties in Elimination Theory, MM Research Preprints, vol. 4. Ins. of Systems Science, Academia Sinica (1991)
Wang, D.: Elimination method. Springer, Heidelberg (2001)
Wang, D.: Zero Decomposition Algorithms for System of Polynomial Equations. Computer Mathematics, pp. 67–70. World Scientific, Singapore (2000)
Gao, X.S., Chou, S.C.: Solving Parametric Algebraic Systems. In: Proc. of ISSAC 1992, pp. 335–341 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, X., Wang, D. (2004). The Projection of Quasi Variety and Its Application on Geometric Theorem Proving and Formula Deduction. In: Winkler, F. (eds) Automated Deduction in Geometry. ADG 2002. Lecture Notes in Computer Science(), vol 2930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24616-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-24616-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20927-0
Online ISBN: 978-3-540-24616-9
eBook Packages: Springer Book Archive