The GeoProver Package for Mechanized (Plane) Geometry Theorem Proving

Version 1.3a

Freezed at Jan 18, 2003

AUTHOR	:	Hans-Gert Graebe
ADDRESS	:	Univ. Leipzig, Institut f. Informatik, D - 04109 Leipzig, Germany
URL	:	http://www.informatik.uni-leipzig.de/~graebe
EMAIL	:	graebe@informatik.uni-leipzig.de

Key Words

Introduction

The GeoProver is a small package for mechanized (plane) geometry manipulations with non degeneracy tracing, available for different CAS platforms (Maple, MuPAD, Mathematica, and Reduce).

It provides the casual user with a couple of procedures that allow him/her to mechanize his/her own geometry proofs. Version 1.1 grew out from a course of lectures for students of computer science on this topic held by the author at the Univ. of Leipzig in fall 1996 and was updated after a similar lecture in spring 1998.

The (completely revised) version 1.2, finished in March 2002, was set up as a generic software project to manage the code for different platforms in a unified way. There is a close relationship to the SymbolicData project (see http://www.symbolicdata.org).

For examples we refer to the test file, but also to the SymbolicData GEO collection. It contains many (generic) proof schemes of geometry theorems, mainly from Chou's book. These proof schemes can be translated to the GeoProver syntax for different platforms with SymbolicData tools.

For version 1.3 the syntax definition (the GeoCode) was separated from the GeoProver implementation. The latter is an implementation of the GeoCode standard using the coordinate method.

Note that function names change with different versions of the GeoCode standard. GeoProver 1.3 implements the GeoCode standard 1.3.

Please send comments, bug reports, hints, wishes, criticisms etc. to the author.

Bibliography

If you have used the GeoProver in the preparation of a publication, please cite it in the following format (in particular, refer explicitely to the used version):

\bibitem{GeoProver}
H.-G. Gr\"abe.
\newblock {\sc GeoProver} -- {A Small Package for Mechanized Plane Geometry
  Theorem Proving}, 1998 -- 2003.
\newblock {With versions for Reduce, Maple, MuPAD and Mathematica.}\\ See
  \url{http://www.informatik.uni-leipzig.de/~compalg/software}.

If you are using BibTeX, you can use the following BibTeX entry

@Misc{GeoProver,
  author =       {Gr\"abe, H.-G.},
  title =        {{\sc GeoProver} -- {A Small Package for
                  Mechanized Plane Geometry Theorem Proving}},
  year =         {1998 -- 2003},
  note =         {{With versions for Reduce, Maple, MuPAD and
                  Mathematica.}\\  See
                  \url{http://www.informatik.uni-leipzig.de/~compalg/software}
                  },
}

Acknowledgements

Malte Witte translated the code of version 1.1 from Reduce to Maple, MuPAD, and Mathematica and compiled many examples for the SymbolicData GEO proof scheme collection, mainly from Chou's book.

Benjamin Friedrich collected examples and solutions with geometric background from IMO contests.