Artifact dcf5e51fdc8395e695a37a809026cca323a34aee6d8c049f2547e479ce25c649:
- Executable file
r38/packages/geometry/geoprover_1_2.htm
— part of check-in
[f2fda60abd]
at
2011-09-02 18:13:33
on branch master
— Some historical releases purely for archival purposes
git-svn-id: https://svn.code.sf.net/p/reduce-algebra/code/trunk/historical@1375 2bfe0521-f11c-4a00-b80e-6202646ff360 (user: arthurcnorman@users.sourceforge.net, size: 3852) [annotate] [blame] [check-ins using] [more...]
<!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>