Books W. W. Bledsoe \& D. W. Loveland (eds.), {\it Automated Theorem Proving: After 25 Years}, Contemporary Mathematics, {\bf 29}(1984). J. Bokovsky \& B. Sturmfels, {\it Computational Synthetic Geometry}, Lec. Notes in Math., no.1355, 1989, Springer-verlag. R. S. Boyer \& J S. Moore, {\it A Computational Logic}, Academic Press, London, 1981. R. S. Boyer \& J S. Moore, {\it A Computational Logic Handbook}, Academic Press, London, 1988. S. C. Chou, {\it Mechanical Geometry Theorem Proving}, D.Reidel Publishing Company, Dordrecht, Netherlands, 1988. H. Crapo, (eds.), {\it Computer-Aided Geometric Reasoning,} I.N.R.I.A., Rocquencourt, 1987. E. W. Disjkstra, {\it Selected Writings on Computing: A Personal Perspective}, Springer-Verlag, Berlin, 1982. D. Kapur (eds), {\it Geometric Reasoning}, MIT Press, 1990. D. Loveland, {\it Automated Theorem Proving: a Logical Basis}, North Holland, Amsterdam, 1978. J. R. Shoenfield, {\it Mathematical Logic}, Addison-Wesley, Publ., 1967. A. Tarski, {\it A Decision Method for Elementary Algebra and Geometry}, Univ. of California Press, Berkeley, Calif., 1951. N. L. White \& T. Mcmillan, Cayley Factorization, {\it Proc. of ISSAC-88}, p.4--8, 1988, ACM Press. L. Wos, R. Overbeek, E. Lusk, \& J. Boyle, {\it Automated Reasoning: Introduction and Applications}, Prentice-Hall, Englewood Cliffs, 1984. Wu Wen-ts\"un, {\it Basic Principles of Mechanical Theorem Proving in Geometries}, Volume I: Part of Elementary Geometries, Science Press, Beijing (in Chinese), 1984. Wu Wen-ts\"un \& X. L. Lu, {\it On Triangles with Equal Angle Bisectors}, People's Educational Press, 1985. J. Z. Zhang, {\it How to Solve Geometry Problems Using Areas,} Shanghai Educational Publishing Inc., (in Chinese) 1982. J. Z. Zhang, {\it A New Approach to Plane Geometry,} Sichuan Educational Publishing Inc., (in Chinese) 1992. J. Z. Zhang \& P. S. Cao, {\it From Education of Mathematics to Mathematics for Education,} Sichuan Educational Publishing Inc., (in Chinese) 1988. Articles Some abbreviations CADE: An International Conference on Automated Deduction. ISSAC: International Symposium on Symbolic and Algebraic Computation. J. R. Anderson, Tuning of Search of the Problem Space for Geometry Proofs, {\it Proc. of Int, Joint Conf. Artificial Intelligence (IJCAI)}, Vancouver, 1981, p.165-170. J. R. Anderson, C. F. Boyle, A. Corbett, \& M. Lewis, The Geometry Tutor, in {\it Proc. of the IJCAI}, Los Angeles, USA, 1985, p. 1--7. W. W. Bledsoe, Some Thoughts on Proof Discovery, in {\it Computers in Mathematics}, eds by D. Chudnovsky and R. D. Jenks, Marcel Dekker INC., 1990. H. Coelho \& L. Pereira, GEOM: a Prolog Geometry Theorem Prover, {\it Lab. Nac. de Engenharia Civ. Meme.}, No. 525, Min. de Habitacao e Obras Publicas, Portugal, 1979. H. Coelho \& L. M. Pereira, Automated Reasoning in Geometry with Prolog, {\it J. of Automated Reasoning}, vol. 2, p. 329-390. M. Davis, The Prehistory and Early History of Automated Deduction, in {\it Automation of Reasoning}, {\it 1}, p.1-28, Springer-Verlag, 1983. E. W. Elcock, Representation of Knowledge in a Geometry Machine, {\it Machine Intelligence}, {\bf 8}, p.11-29. T.G. Evans, A Heuristic Program to Solve Geometry Analogy Problems, {\it Semantic Ubform. Proc.}, (ed), Minsky, M.I.T. Press, 1968. D. Fearnley-Sander, Using and Computing Symmetry in Geometry Proofs, {\it Proc. Conf. Artificial Intelligence and the Simulation of Behavior}, ed. P. Ross. D. Fearnley-Sander, The Idea of a Diagram, in {\it Resolution of Equations in Algebra}, (eds. H. Ait-Kaci and M. Nivat), Academic Press, 1989. H. Gelernter, J. R. Hanson, \& D. W. Loveland, Empirical Explorations of the Geometry-theorem Proving Machine, {\it Proc. West. Joint Computer Conf.}, 143-147, 1960. H. Gelernter, Realization of a Geometry-Theorem Proving Machine, {\it Computers and Thought}, eds. E.A. Feigenbaum, J. Feldman, p. 134-152, Mcgraw Hill. H. Gelernter \& N. Rochester, Intelligent Behavior in Problem-Solving Machines, {\it IBM Journal}, p. 336-345, Oct., 1958. H. Gelernter, A Note on Syntactic Symmetry and the Manipulation of Formal Systems by Computers, {\it Information and Control}, {\bf 2}, p.80-89, 1959. H. Goldstein, Elementary Geometry Theorem Proving, MIT, AI LAB memo no. 280, 1973. % P. C. Gilmore, An Examination of the Geometry Theorem Proving Machine, {\it Artificial Intelligence}, {\bf 1}, p. 171--187. J. A. Goguen, Modular Algebraic Specification of Some Basic Geometrical Constructions, {\it Artificial Intelligence}, {\bf 37}, 121--156, 1988. B. Gr\"unbaum \& G. C. Shephard, From Menelaus to Computer Assisted Proofs in Geometry, preprint, 1993. M. Hardzikadic, F. Lichtenberger, \& D. Y. Y. Yun, An Application of Knowledge Based Technology in Education: a Geometry Theorem Prover, {\it Proc. of SYMSAC'86}, ed. B.W. Char, p. 141-147, ACM Press. T. Havel, The Use of Distances as Coordinates in Computer-Aided Proofs of Theorems in Euclidean Geometry, IMA Preprint No. 389, University of Minnesota, 1988. T. J. Kelanic, Theorem-proving with Euclid, {\it Creative Computing}, {\bf 4}, p.60-63, 1978. K. R. Koedinger \& J. R. Anderson, Abstract Planning and Perceptual Chunks: Elements of Expertise in Geometry, {\it Cognitive Science}, 14, 511-550, (1990). D. Loveland, Automated Theorem Proving: a Quarter-centrex Review, {\it Automated Theorem Proving: After 25 years}, American Mathematics Society, Contemporary Mathematics, V. 29, 1984, p.1-45. D. Loveland \& M. E. Stikel, A Hole in Goal Trees: Some Guidance from Resolution Theory, {\it IEEE Trans. on Computers}, {\bf C-25}, p.225-341, 1976. J. D. Mccharen, R. A. Overbeek, \& L. A. Wos, Problems and Experiments for and with Automated Theorem-proving Programs, {\it IEEE Trans. on Computers}, C-25:773-782, 1976. T. F. Mcdougal \& K. J. Hammond, Representing and Using Procedural Knowledge to Build Geometry Proofs, {\it Proc. of AAAI} , 1993. R. Padmanabhan \& W. McCune, Automated Reasoning about Cubic Curves, {\it Computers and Mathematics with Applications}, 29(2), p.17-26,1995. T. F. McDougal, Diagrammatic Reasoning in Plane Geometry, Preprint, University of Chicago, 1993. A. J. Nevins, Plane Geometry Theorem Proving Using Forward Chaining, {\it Artificial Intelligence}, {\bf 6}, 1-23, 1975. R. Reiter, A Semantically Guided Deductive System for Automatic Theorem Proving, {\it IEEE Tras. on Computers}, vol C-25, No.4, p.328-334. J. Robinson, A Machine-oriented Proof Procedure, {\it Theoria}, 1960, p.102-139. A. Robinson, Proving a Theorem (as done by Man, Logician, or machine), in {\it Automation of Reasoning}, ed. by J. Siekmann and G. Wrightson, p.74-78, 1983, Springer-Verlag. M. Stickel, A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler, {\it J. of Automated Reasoning}, 4(4), 353--380, 1985. J. D. Starkey, EUCLID: A Program Which Conjectures, Provers and Evaluates Theorems in Elementary Geometry, Univ. Microfilms, 75-2780. S. Ullman, A Model-driven Geometry Theorem Prover, AI Lab Memo No. 321, MIT, 1975. H. Wang, Computer Theorem Proving and Artificial Intelligence, {\it Automated Theorem Proving: After 25 years}, A.M.S., Contemporary Mathematics, 29(1984), 1--27. B. Welham, Geometry Problem Solving, Res. Rep. No. 14, Dept. of AI, Uinv. of Edingburgh, UK. L. Wos, et all, An Overview of Automated Reasoning and Related Fields, J. of Automated Reasoning, {\bf 1}, 5-48, 1985. L. Xu \& J. Chen, AUTOBASE: A System Which Automatically Establishes the Geometry Knowledge Base, {\it Proc. COMPINT 85: Computer Aides Technologies}, p. 708-714, 1985, IEEE Comp. Soc. Press. J. Z. Zhang, S. C. Chou, \& X. S. Gao, Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, I. The Hilbert Intersection Point Theorems, TR-92-3, Department of Computer Science, WSU, 1992. (to appear in {\it Annals of Mathematics and Artificial Intelligence}) J. R. Anderson, C. F. Boyle, A. Corbett, \& M. Lewis, The Geometry Tutor, in {\it Proc. of the IJCAI}, Los Angeles, USA, 1985, p. 1--7. H. Coelho \& L. M. Pereira, Automated Reasoning in Geometry with Prolog, {\it J. of Automated Reasoning}, vol. 2, p. 329-390. E. W. Elcock, Representation of Knowledge in a Geometry Machine, {\it Machine Intelligence}, {\bf 8}, p.11-29. H. Gelernter, A Note on Syntactic Symmetry and the Manipulation of Formal Systems by Computers, {\it Information and Control}, {\bf 2}, p.80-89, 1959. H. Gelernter, J. R. Hanson, \& D. W. Loveland, Empirical Explorations of the Geometry-theorem Proving Machine, {\it Proc. West. Joint Computer Conf.}, 143-147, 1960. P. C. Gilmore, An Examination of the Geometry Theorem Proving Machine, {\it Artificial Intelligence}, {\bf 1}, p. 171--187. K. R. Koedinger \& J. R. Anderson, Abstract Planning and Perceptual Chunks: Elements of Expertise in Geometry, {\it Cognitive Science}, 14, 511-550, (1990). A. J. Nevins, Plane Geometry Theorem Proving Using Forward Chaining, {\it Artificial Intelligence}, {\bf 6}, 1-23. R. Reiter, A Semantically Guided Deductive System for Automatic Theorem Proving, {\it IEEE Tras. on Computers}, vol C-25, No.4, p.328-334.