\documentstyle [11pt]{article}
\title{Geometry Theorem-Proving and Geometry Problem-Solving, Old and New}
\author{\sc Wu Wen-ts\"un \\ 
\sc (Institute of Systems Science, Academia Sinica)}
\date{} 
\begin{document}
\maketitle

\vskip 1cm
\centerline{\bf Abstract}

\medskip
      The geometry theorem-proving in ancient Greece is well-known.  As
   for in ancient China, one considered usually geometry problem-solving
   rather than geometry theorem-proving, and for the latter the theorems
   to be proved were usually in the form of formulae.  Furthermore, 
   instead of set of axioms, the ancient Chinese formulated rather some
   simple and plausible principles and then proved the formulae or solved
   the problems by logical reasoning.

      A turning point occurred in Song Dynasty (+960, +1274) and Yuan
   Dynasty (+1271, +1368).  During that period the notions of {\em Heaven
   Element}, {\em Earth Element}, etc., (= unknowns $x,y$, etc.), together 
   with allied notions of polynomials and methods of elimination, were 
   introduced. Geometry was thus algebrized to be applied to solving of 
   geometry problems.  Numerous examples may be found in some still existant
   classics.

      The algebrization of geometry was systematized owing to the creation
   of analytic geometry by R.\ Descartes.  Descartes emphasized in his 1637
   classic the geometry problem-solving rather than geometry 
   theorem-proving which was the same spirit in ancient China. The analytic
   geometry also permits to prove geometry theorems by mere computations
   in contrast to the proving by purely geometrical reasoning of Euclid.
   This computational method of proving geometry theorems lacked however
   a general way of dealing with the associated system of equations usually
   in embarrassing confused form.

      A turning point occurred in the time of Hilbert.  In fact, in his 1899
   classic there was some obscure passages which, after some clarification
   and extension, may be interpreted as a {\em mechanical\/} way of geometrical
   theorem-proving.  The proving, being computational and mechanical, can
   be carried out on a modern computer.  A lot of difficult theorems have
   thus been proved on the computer in a straightforward and trivial way.

      In recent years the Chinese mathematicians, mainly in MMRC (Math.\
   Mech.\ Res.\ Center), have developed a general {\em mechanization 
   method\/} for geometry theorem-proving and geometry problem-solving.  
   Among the applications considered we may cite in particular:
\begin{enumerate}
\item  Automated deduction of unknown relations and geometric loci.

\item  Enumerative geometry and computational geometry.

\item  Inequalities and optimization problems.

\item  Mechanism studies.

\item  CAGD: surface-fitting.
\end{enumerate}

      Numerous examples may be given to illustrate the various methods of
   geometry theorem-proving and geometry problem-solving, both old and new.

\end{document}
