The GeoProver Package for Mechanized (Plane) Geometry Theorem Proving

Version 1.2

Freezed at March 6, 2002

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

geometry theorem proving

Introduction

The GeoProver (formerly GEOMETRY) 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. Even most of the function names changed due to more concise naming conventions. There is a close relationship to the SymbolicData project (see http://www.symbolicdata.org/).

For examples we refer to the SymbolicData GEO table that contains many proof schemes of geometry theorems, mainly from Chou's book, and an interface from SymbolicData to the GeoProver.

Comments, bug reports, hints, wishes, criticisms etc. are welcome. Please send them 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} 1.2 -- {A Small Package for Mechanized Plane Geometry
  Theorem Proving}, 2002.
\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} 1.2 -- {A Small Package for
                  Mechanized Plane Geometry Theorem Proving}},
  year =         {2002},
  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 filled the SymbolicData GEO table with many examples from mechanized geometry theorem proving, mainly from Chou's book.

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

Upgrade Information

Proof schemes from Version 1.1 require an upgrade. There is a perl script changeFiles.pl to support this upgrade.