\begin{section}{Abschluss und Benchmark}

%Allgemeiner noch was schreiben%%%%%%%%%%%%%%%%%%%%%%%%
In dieser Arbeit wurde eine Methode zum automatischen Beweisen von geometrischen S{\"a}tzen eingef{\"u}hrt, begr{\"u}ndet und an
Beispielen getestet. Mit diesen Methoden ist es sehr leicht m{\"o}glich, weitere geometrische S{\"a}tze zu beweisen. Um die
Zeit bis zum Beweis eines Satzes einmal genau zu bestimmen, habe ich den letzten Beweis, den des Satzes vom
Exeterpunkt, mit der \anf{Uhr in der Hand} durchgef{\"u}hrt. Als ich den Satz im Internet fand, hatte ich die Hoffnung,
dass sein Beweis schwer ist, da es ein sehr neuer Satz ist. Es erwies sich auch als sehr schwer, da die Quelle den Satz
falsch angegeben hatte. Nachdem ich eine korrekte Version des Satzes gefunden hatte, habe ich mit GeoNext
\cite{geonext} eine Zeichnung angefertigt. Dies war in einer Viertelstunde erledigt, und ich konnte zu \ma\ {\"u}bergehen,
um den Satz in meinen automatischen Beweiser einzugeben. Hierf{\"u}r habe ich 13 Minuten gebraucht, inklusive des
automatischen Beweises.
Leider erwies sich der Satz als nicht besonders kniffelig f{\"u}r den Beweiser.\\
Nach dieser Zeitmessung bei der Eingabe will ich noch auf einen kleinen Benchmark der verschiedenen
Computeralgebrasysteme eingehen -- man kann \gbn\ ja auf verschiedenen Systemen berechnen. Die Erzeugung der Polynome
{\"u}berlasse ich dabei ganz \ma. Der Satz von Morley ist am besten als Benchmark geeignet, da er die l{\"a}ngste Rechenzeit
ben{\"o}tigt, jedenfalls ist dies in \ma\ der Fall. Um wenigstens einen kleinen Vergleich zu haben, gebe ich zwei Zeiten
von \gb berechnungen an: Die Zeit zum Beweis des erweiterten Satzes von Morley und die Zeit zur Berechnung der \gb\
%der \anf{kleineren Menge} von Polynomen aus den Voraussetzungen dieses Satzes
des definierenden Ideals (die Polynome sind in Anhang \ref{Polynome f{\"u}r den Benchmarktest} nochmals verzeichnet).

\begin{tabular}{|c|c|c|}
  \hline
  % after \\: \hline or \cline{col1-col2} \cline{col3-col4} ...
  Computeralgebrasystem & Beweis & Definierendes Ideal \\
  \hline
  Magma 2.11 & 380 ms & 310 ms \\
  Maple 9 & 3200 ms & 1300 ms \\
  \ma\ 5.0 & 80105 ms & 6409 ms \\
  Reduce 3.7 & 70 ms & nach 30 min abgebrochen \\
  \hline
\end{tabular}

Diese einzelnen Ergebnisse haben nat{\"u}rlich keine allgemeine Aussagekraft {\"u}ber die Geschwindigkeit eines
Computeralgebrasystems. Um einen seri{\"o}sen Vergleich anzustellen, mussten alle Computeralgebrasysteme auf einem Rechner
laufen. Daf{\"u}r beschaffte ich mir Demoversionen aus dem Internet bzw. {\"u}ber Kontakte an der Universit{\"a}t Kassel. Im Anhang
\ref{Polynome f{\"u}r den Benchmarktest} finden sich die Adressen, bei welchen man diese Demoversionen erh{\"a}lt. Die meisten
dieser Versionen sind, mit kleineren Einschr{\"a}nkungen, 30 Tage lauff{\"a}hig. Maple bildet hierbei eine Ausnahme; die
Einschr{\"a}nkungen lassen kein Speichern und \anf{Copy\&Paste} zu; damit ist vern{\"u}nftiges Arbeiten nicht m{\"o}glich. Ich habe
ein Notebook mit Mobile Pentium IV 2.2 GHz und 1 GB RAM verwendet, um die Berechnungen durchzuf{\"u}hren. Was besonders
auff{\"a}llt, ist die kurze Rechenzeit von Reduce f{\"u}r den Beweis im Gegensatz zu den anderen Systemen, die alle die \gb\
%der \anf{kleineren Menge}
des definierenden Ideals schneller berechnen.

Dieser Benchmark hat mich neugierig gemacht, ob Reduce mit seiner hohen Geschwindigkeit vielleicht auch in der Lage
sei, den Satz von Morley direkt zu beweisen. Daher habe ich die Herleitung der Polynome f{\"u}r diesen Beweis noch einmal
durchgef{\"u}hrt (siehe Anhang \ref{Direkter Beweis Satz von Morley}) und nach Reduce portiert. In der Tat ist Reduce in
der Lage, die \gb\ zu berechnen. Der Beweis des Satz von Morley ist damit direkt gelungen! Es dauerte nur 50 ms, bis
die Berechnung beendet war. Im Gegensatz dazu ist es mir nicht gelungen, diesen Beweis mit einem anderen
Computeralgebrasystem zu verifizieren. Weder Magma noch \ma\ waren in der Lage, innerhalb von 12 Stunden eine L{\"o}sung zu
berechnen.
\end{section}
