<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<!-- saved from url=(0076)http://www.informatik.uni-leipzig.de/~compalg/software/geoprover/Readme.html -->
<HTML><HEAD><TITLE>GeoProver version 1.2</TITLE>
<META content="text/html; charset=windows-1252" http-equiv=Content-Type>
<META content="MSHTML 5.00.2314.1000" name=GENERATOR></HEAD>
<BODY>
<H1 align=center>The GeoProver Package for Mechanized (Plane) Geometry Theorem
Proving
<P>Version 1.2</H1>
<P>Freezed at March 6, 2002
<H3 align=center>
<TABLE>
<TBODY>
<TR>
<TD>AUTHOR
<TD>:
<TD>Hans-Gert Graebe
<TR>
<TD>ADDRESS
<TD>:
<TD>Univ. Leipzig, Institut f. Informatik, D - 04109 Leipzig, Germany
<TR>
<TD>URL
<TD>:
<TD><A
href="http://www.informatik.uni-leipzig.de/~graebe">http://www.informatik.uni-leipzig.de/~graebe</A>
<TR>
<TD>EMAIL
<TD>:
<TD>graebe@informatik.uni-leipzig.de </TR></TBODY></TABLE></H3>
<H4>Key Words</H4>geometry theorem proving
<H4>Introduction</H4>
<P>The <B>GeoProver</B> (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).</P>
<P>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. </P>
<P>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 <A
href="http://www.symbolicdata.org/">http://www.symbolicdata.org/</A>). </P>
<P>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.</P>
<P>Comments, bug reports, hints, wishes, criticisms etc. are welcome. Please
send them to the author.</P>
<H4>Bibliography</H4>
<P>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): </P><PRE>\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}.
</PRE>
<P>If you are using BibTeX, you can use the following BibTeX entry</P><PRE>@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}
},
}
</PRE>
<H4>Acknowledgements</H4>
<P>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.</P>
<P>Benjamin Friedrich collected examples and solutions with geometric background
from IMO contests.</P>
<H4>Upgrade Information</H4>Proof schemes from Version 1.1 require an upgrade.
There is a perl script <TT>changeFiles.pl</TT> to support this upgrade.
</BODY></HTML>