reduce-algebra
/
reduce-historical
дзеркало git://github.com/reduce-algebra/reduce-historical


			
				
					
						
						
							12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182
							<!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>