D. S. Arnon, Geometric Reasoning with Logic and Algebra, {\it Artificial Intelligence}, {\bf 37}(1988) 37--60. D. S. Arnon \& M. Mignotte, On Mechanical Quantifier Elimination for Elementary Algebra and Geometry, {\it J. Symbolic Computation}, {\bf 5}(1988), p.237--259. B. Buchberger, Gr\"obner Bases: an Algorithmic Method in Polynomial Ideal Theory, {\it Recent Trends in Multidimensional Systems theory}, D.Reidel Publ. Comp., 1985. B. Buchberger, Applications of Gr\"obner Bases in Non-linear Computational Geometry, LNCS No 296, R.JanBen (Ed.), p. 52--80, Springer-Verlag, 1987. B. Buchberger, G. E. Collins, \& B. Kutzler, Algebraic Methods for Geometric Reasoning, {\it Annual Review of Computer Science}, Vol. 3. E. Cerutti, P. J. Davis, FORMAC Meets Pappus, {\it The American Mathematical Monthly}, {\bf 76}:895--905, 1969. S. C. Chou, Proving Elementary Geometry Theorems Using Wu's Algorithm, {\it Automated Theorem Proving: After 25 years}, American Mathematics Society, Contemporary Mathematics, 29(1984), 243--286. S. C. Chou, Proving and Discovering Geometry Theorems Using Wu's Method, Ph.D Thesis, Dept. of Math., University of Texas, Austin, 1985. S. C. Chou, GEO-Prover - A Geometry Theorem Prover Developed at UT, {\it Proc. of CADE-8,} Oxford, 1986. S. C. Chou, A Method for Mechanical Deriving of Formulas in Elementary Geometry, {\it J. of Automated Reasoning}, {\bf 3}(1987), 291----299. S. C. Chou, An Introduction to Wu's Method for Mechanical Theorem Proving in Geometry, {\it J. of Automated Reasoning}, {\bf 4}(1988), p.237-267. S. C. Chou, Automated in Geometries Using the Characteristic Set Method and Gr\"obner basis Method, {\it Proc. of ISSAC-90}, p255-260. S. C. Chou \& X. S. Gao, Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving, {\it Proc. CADE-10}, M.E. Stickel (Ed.) pp 207--220, Lect. Notes in Comp. Sci., No. 449, Springer-Verlag, 1990. S. C. Chou \& X. S. Gao, Mechanical Formula Derivation in Elementary Geometries, {\it Proc. ISSAC-90}, ACM, New York, 1990, p. 265--270. S. C. Chou \& X. S. Gao, Proving Constructive Geometry Statements, {\it Proc. CADE-11}, D. Kapur (eds), p. 20--34, Lect. Notes on Comp. Sci., No. 607, Springer-Verlag, 1992. S. C. Chou \& X. S. Gao, Mechanical Theorem Proving in Riemann Geometry, to appear in {\it Proc. of Nankai Seminar}, 1992, World Science, Singapore. S. C. Chou \& X.S. Gao, A Collection of 120 Computer Solved Geometry Problems in Mechanical Formula Derivation, TR-89-22, Computer Sciences Department, The University of Texas at Austin, August 1989. S.C. Chou \& X.S. Gao, The Computer Searches for Pascal Conics, {\it An International Journal of Computers \& Mathematical Applications}, Vol. 29, No. 2, pp. 63-71, 1995, Elsevier Science Ltd. (Mathematics Review 95i:51003) S.C. Chou \& X.S. Gao, A Survey of Geometric Reasoning Using Algebraic Methods, ``Learning and Geometry: Computational Approaches'', D.W. Kueker and Carl Smith Eds., p. 97--120, Birkhauser, 1996. S. C. Chou, X. S. Gao \& D. S. Arnon, On the Mechanical Proof of Geometry Theorems Involving Inequalities, {\it Advances in Computing Research,} {\bf 6}, (ed. C.M. Hoffmann), p.139-181, 1992, JAI Press INc, Greenwich, USA. S. C. Chou \& H. P. Ko, On the Mechanical Theorem Proving in Minkowskian Plane Geometry, {\it Proc. of Symp. of Logic in Computer Science}, pp187-192, 1986. S. C. Chou \& W. F. Schelter, Proving Geometry Theorem with Rewrite Rules, {\it J. of Automated Reasoning} {\bf 4}, 253-273, 1986. S. C. Chou, W. Schelter \& G. J. Yang, Characteristic Sets and Gr\"obner Bases in Geometry Theorem Proving, {\it Resolution of Equations in Algebraic Structure}, Vol. I, pp33--92, Academic Press, Boston, 1989. S. C. Chou \& J. G. Yang, On the Algebraic Formulation of Certain Geometry Statements and Mechanical Geometry Theorem Proving, {\it Algorithmica}, {\bf 4}, 1989, 237-262. S. C. Chou and J. G. Yang, An Algorithm for Constructing Gr\"bner Bases from Characteristic Sets, {\it Algorithmica}, 5, 147--154, 1990. S. C. Chou \& W. F. Schelter, Proving Geometry Theorems with Rewrite Rules, {\it J. of Automated Reasoning} {\bf 4}, 253-273, 1986. G. E. Collins, Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition, {\it Lect. Notes Comp. Sci.} 33, 134--183, Springer-Verlag, 1975. D. A. Cyrluk, R. M. Harris, \& D. Kapur, GEOMETER, A Theorem Prover for Algebraic Geometry, {\it Proc. of CADE-9}, Argonne, 1988, L.N.C.S., Vol. 310, p.770-771, Springer. X. S. Gao, Trigonometric Identities and Mechanical Theorem Proving in Elementary Geometries, {\it J. Sys. Sci. \& Math. Scis.} No.3 1987, (in Chinese). X. S. Gao, Constructive Methods for Polynomial Sets and Their Applications, PhD Thesis, Institute of Systems Science, Academia Sinica, 1988 (in Chinese). X. S. Gao, Transcendental Functions and Mechanical Theorem Proving in Elementary Geometries, {\it J. of Automated Reasoning}, {\bf 6}:403-417, 1990, Kluwer Academic Publishers. X. S. Gao, Transformation Theorems among Caley-Klein Geometries, {\it J. of Sys. Sci. and Math. Sci.}, 1992, {\bf 3}: 260--273. X. S. Gao, An Introduction to Wu's Method of Mechanical Geometry Theorem Proving, {\it IFIP Transaction on Automated Reasoning}, p.13--21, North-Holland, 1993. X.S. Gao \& S. C. Chou, On the Dimension for Arbitrary Ascending Chains, {\it Chinese Bull. of Scis.}, vol. 38, pp.396--399, 1993. X. S. Gao, Y. Li, D. D. Lin, \& X. S. Liu, A Prover Based on Wu's Method, {\it Proc. of International Workshop on Mathematics Mechanization}, Beijing, International Academic Publishers, p.201--205, 1992. X. S. Gao \& D. K. Wang, On the Automatic Derivation of a Set of Geometric Formulae, {\it Journal of Geometry}, vol. 53, p.79-88, 1995. Hitoshi Iba \& Hirochika Inoue, Geometric Reasoning Based on Algebraic Method Part I: Application of Wu's Method to Geometric Reasoning, Journal of Artificial Intelligence, Japan, vol5, No 3, p. 46--56. Hitoshi Iba \& Hirochika Inoue, Geometric Reasoning Based on Algebraic Method Part II: Solution t Locus Problems, Journal of Artificial Intelligence, Japan, vol5, No 3, p. 57--69. C. Hoffmann (eds), {\it Issues in Robotics and Nonlinear Geometry}, {\it Advances in Computing Research,} vol. 6, JAI Press INc, Greenwich, USA. H. Hong, Simple Solution Formula Construction in Cylindrical Algebraic Decomposition based on Quantifier Elimination, {\it Proc. of ISAAC'92}, p. 177--188, 1992, ACM Press. J. W. Hong, Can a Geometry Theorem Be Proved by an Example?, {\it Scientia Sinica,} {\bf 29}, 824--834, 1986. J. W. Hong, How Fast the Algebraic Approximation Can be?, Scientia Sinica, {\bf 29}, 813--823, 1986. M. A. Hussain, M. A. Drew, \& M. A. Noble, Using a Computer for Automatic Proving of Geometric Theorems, {\it Computers in Mechanical Engineering}, {\bf 5}, p. 56-69. M. Kalkbrener, {\it Three Contributions to Elimination Theory}, Phd Thesis, RISC, Linz, 1991. M. Kalkbrener, A Generalized Euclidean Algorithm for Geometry Theorem Proving, Mathematik Report No. 93-02, ETH Zurich. D. Kapur, Geometry Theorem Proving Using Hilbert's Nullstellensatz, {\it Proc. of SYMSAC'86}, Waterloo, 1986, 202--208. D. Kapur, Using Gr\"obnre Bases tp Reason about Geometry Problems, {\it J. of Symbolic Computation}, {\bf 2}, p.399-408. D. Kapur, A Refutational Approach to Geometry Theorem Proving, {\it Artificial Intelligence}, {\bf 37}, 61-94, 1988. D. Kapur \& J. L. Mundy, Wu's Method and Its Application to Perspective Viewing, {\it Artificial Intelligence}, {\bf 37}, 15--36, 1988. D. Kapur \& H. K. Wan, Refutational Proofs of Geometry Theorems via Characteristic Sets, {\it Proc. of ISSAC-90}, 277-284. H. P. Ko, Geometry Theorem Proving by Decomposition of Quasi-Algebraic Sets: An Application of the Ritt-Wu Principle, {\it Artificial Intelligence}, 37(1988) 95--120. H. P. Ko \& S. C. Chou, A Decision Method for Certain Algebraic Problems, {\it Rocky Mountain Journal of Mathematics,} 19(3), 1989, 709-724. H. P. Ko \& M. A. Hussain, ALGE-Prover, an Algebraic Geometry Theorem Proving Softeware, Technical Report, 85CRD139, General Electric Company, 1985. K. Kusche, B. Kutzler, \& H. Mayr, Implementation of a Geometry Theorem Proving Package in Scratchpad II, {\it Proc. of EUROCAL'87}, Leipzig, 1987, ed. J. Davenport, L.N.C.S., Springer. B. Kutzler, Algebraic Approaches to Automated Geometry Theorem Proving, Phd Thesis, Johnnes Kepler University, 1988. B. Kutzler, Careful Algebraic Translations of Geometry Theorems, {\it Proc. of ISSAC-89}, 254-263. B. Kutzler \& S. Stifter, Automated Geometry Theorem Proving Using Buchberger's Algorithm, {\it Proc. of SYMSAC'86}, Waterloo, 1986, 209--214. B. Kutzler \& S. Stifter, On the Application of Buchberger's Algorithm to Automated Geometry Theorem Proving, {\it J. of Symbolic Computation}, {\bf 2}, p.389--397. B. Kutzler \& S. Stifter, A Geometry Theorem Prover Based on Buchberger's Algorithm, {\it Proc. CADE-7}, 1987, Oxford, ed. J. H. Siekmann, L.N.C.S., vol. 230, p.693--694. B. Kutzler \& S. Stifter, Collection of Computerized Proof of Geometry Theorems, Technical Report 87-25, Research Institute for Symbolic Computation, 1987. Z. M. Li, Mechanical Theorem-Proving of the Local Theory of the Surfaces, p.102-p120, MM-Preprints, NO. 6, MMRC. D. D. Lin \& Z. J. Liu, Some Results on Theorem Proving in Finite Geometry, {\it proc. IWMM'92}, Inter. Academic Pub., Beijing, 1992. N. F. McPhee, Mechanical Proving Geometry Theorems using Wu's Method and Collins' Method, Phd Thesis, 1993, Univ. of Texas at Austin. N. Mcphee, S.C. Chou, \& X.S. Gao, A Combination of Ritt-Wu's Method and Collins' Method, {\it Proc. of CADE-12}, p.401-415, France, 1994. A. Seidenberg, A New Decision Method for Elementary Algebra, {\it Annals of Math.}, V. 60, 1954, p.365--371. A. Seidenberg, An Elimination Theory for Differential Algebra, {\it Univ. California Publication in Math.}, 3 (1956), 31-65. A. Rege, A Complete and Practical Algorithm for Geometric Theorem Proving, Preprint, Computer Science Division, Univ. of California at Berkeley, 1995. S. Stifter, Geometry Theorem Proving in Vector Spaces by Means of Gr\"obner Bases, {\it Proc. of ISSAC-93}, Kiev, ACM Press, p. 301--310,1993. T. E. Stokes, {\it On the Algebraic and Algorithmic Properties of Some Generalized Algebras}, Phd Thesis, University of Tasmania, 1990. B. Sturmfels, Computational Synthetic Geometry, Ph.D. Dissertation, University of Washington, 1987. M. J. Swain \& J. L. Mundy, Experiments in Using a Theorem Prover to Prove and Develop Geometrical Theorems in Computer Vision, {\it Proc. of IEEE Int. Robotcs and Automation}, p.280-285, IEEE Computer Sci Press. D. M. Wang, A New Theorem Discovered by Computer Prover, J. of Geometry, vol. {\bf 36}, pp173-182, 1989. D. M. Wang \& X. S. Gao, Geometry Theorems Proved Mechanically Using Wu's Method, Part on Elementary Geometries, MM preprint No2, 1987. D. M. Wang \& S. Hu, Mechanical Proving System for Constructible Theorems in Elementary Geometry, J. Sys. Sci. \& Math. Scis., 7(1987). F. Winkler, A Geometrical Decision Algorithm Based on the Gr\"obner Basis Algorithm, {\it Proc. of ISSAC-88}, Italy, p.4--8, 1988. F. Winkler, Automated Theorem Proving in Nonlinear Geometry, {\it Advances in Computing Research,} vol. 6, (ed. C.M. Hoffmann), o. 183-198, 1992, JAI Press INc, Greenwich, USA. L. Yang, On the Area Coordinates, in {\it Essays on Elementary Mathematics and Education}, 1979, Shanghai Educational Press. L. Yang, A New Method of Automated Theorem Proving, in {\it The Mathematical Revolution Inspired by Computing,} J.H. Johnson and M.J. Loomes (eds), Oxford University Press 1991. p.115-126 L. Yang \& J. Z. Zhang, Searching Dependency Between Algebraic Equations: An Algorithm Applied to Automated Reasoning, I.C.T.P. preprint IC/91/6, Trieste; also in {\it Artificial Intelligence in Mathematics}, IMA Conference Proceedings, Oxford University Press, to appear. L. Yang, J.Z. Zhang, \& X.R. Hou, A Criterion of Dependency Between Algebraic Equations and Its Applications, {\it Proc. of the 1992 international Workshop on Mechanization of Mathematics}, p.110-134, Inter. Academic Publishers. L. Yang, J. Z. Zhang \& C. Z. Li, A Prover for Parallel Numerical Verification of a Class of Constructive Geometry Theorems', Proceedings of the 1992 International Workshop on Mathematics Mechanization, W. Wu and M. Cheng (eds), International Academic Publishers 1992. p.244-250. J. Z. Zhang \& L. Yang, Principles of Parallel Numerical Method and Single-instance Method of Mechanical Theorem Proving', {\it Math. in Practice and Theory,} 1, 34-43, 1989. A Method to Overcome the Reducibility Difficulty in Mechanical Theorem Proving, I.C.T.P. preprint IC/89/263. J. Z. Zhang, L. Yang \& M. Deng, The Parallel Numerical Method of Mechanical Theorem Proving, {\it Theoretical Computer Science}\/ {\bf 74}, 253-271 (1990). J. Z. Zhang, L. Yang \& X. R.Hou, W.E., A Complete Method for Automated Theorem Proving in Geometry', {\it J. Sys.Sci. and Math.Sci.}\/ (Chinese ed), to appear. J. Z. Zhang, L. Yang \& X. R. Hou, The Sub-resultant Method for Automated Theorem Proving, {\it J. Sys.Sci. and Math.Sci.}\/ (Chinese ed), to appear. J. Z. Zhang, L. Yang \& X. R. Hou, A Note on Wu Wen-ts\"un's Non-degenerate Condition, {\it Bulletin of Science,}\/ {\bf 37}:19(1992),1821-1826. L. Yang, J. Z. Zhang \& X. R. Hou, An Efficient Decomposition Algorithm for Geometry Theorem Proving Without Factorization, MM Research Report, 1993. J. Z. Zhang, L. Yang, \& X. R. Hou, A Note on Wu Wen-Ts\"un's Non-degenerate Conditions, IC/91/160, International Center for Theoretic Physics.