\begin{chapter}{Einleitung}
In der Mathematik ist automatisches Beweisen ein umstrittenes Thema. Der erste Satz, der nur mit dem Computer bewiesen
werden konnte, ist das Vier-Farben-Problem von Francis Guthrie aus dem Jahre 1853.
%Der Beweis von Appel und Haken stammt aus dem Jahre 1977. Sie konnten die Anzahl der problematischen F{\"a}lle von
%unendlich auf 1936 reduzieren,
Erst 1977 konnten Appel und Haken einen Beweis finden. Er reduzierte die Anzahl der problematischen F{\"a}lle von Unendlich
auf 1936, die durch einen Computer einzeln gepr{\"u}ft wurden. Inzwischen ist es zwar gelungen, die Anzahl der F{\"a}lle auf
633 zu reduzieren, aber an ein menschliches
\anf{Nachrechnen} ist bei weitem nicht zu denken. Daher ist der Vier-Farben-Satz bis heute nicht von allen Mathematikern als bewiesen anerkannt.\\
Im Bereich der Geometrie haben wir es etwas einfacher: Da f{\"u}r viele S{\"a}tze bereits ein \anf{klassischer} Beweis
existiert, k{\"o}nnen wir die Methoden dort ausprobieren. In der Geometrie klassifiziert man die automatischen Beweiser im
Wesentlichen in folgende drei Kategorien: die auf Logik basierenden, die algebraischen und die randomisierten Beweiser.\\
Letztere spielen eine Anzahl von Beispielen durch und schlie{\ss}en mit einer gewissen Irrtumswahrscheinlichkeit daraus,
dass ein Satz wahr oder falsch ist. Dieses Verfahren ist in dem dynamischen Geometrieprogramm
Cinderella implementiert \cite{cinderella}.\\
Bei der algebraischen Methode werden den geometrischen Eigenschaften Polynome zugeordnet.
Dabei wird ein Verfahren angewandt, das zeigt, ob der Satz wahr ist.\\
Auf zwei Verfahren will ich hier n{\"a}her eingehen: die Methode von Wu und die \gbm. Die Methode von Wu beruht im
Wesentlichen auf einer Verfeinerung der Polynomdivision in mehreren Variablen. Dieses Verfahren hat Chou genutzt, um
eine gro{\ss}e Sammlung an geometrischen S{\"a}tzen zu beweisen \cite{Chou88}. F{\"u}r einzelne Beispiele verwendet auch er die
\gbm, welche auf dem gleichnamigen Algorithmus von Bruno Buchberger fu{\ss}t und verwendet wird, um das
\anf{Ideal-Membership-Problem} zu l{\"o}sen.

Diese Arbeit ist in drei thematische Bereiche untergliedert.

Wir beginnen mit den grundlegenden Definitionen und S{\"a}tzen, die zum Umgang mit Geometrie und \gbn\ notwendig sind. Nach
der Einf{\"u}hrung der geometrischen Bezeichnungen gehen wir zu den Variet{\"a}ten, Idealen und ihren Zusammenh{\"a}ngen {\"u}ber. Dann
f{\"u}hren wir Monomordnungen und \gbn\ ein. Das erste Kapitel wird abgerundet von den S{\"a}tzen {\"u}ber \anf{strikte} und
\anf{generalisierte} Folgerung.

Im zweiten Kapitel beginnen wir mit einem Beispiel und f{\"u}hren dabei unabh{\"a}ngige und abh{\"a}ngige Punkte und Koordinaten
ein. Als n{\"a}chstes {\"u}bersetzen wir die geometrischen Eigenschaften dieses Beispiels in Polynome. Das Beispiel endet mit
einem \anf{Ideal-Membership-Test} und der Einf{\"u}hrung von degenerierten F{\"a}llen.

Der darauf folgende Abschnitt hei{\ss}t \anf{Umsetzung in \ma}. Dort behandeln wir die Benutzung von \gbn\ in \ma. Wir
f{\"u}hren die Bibliothek GeoBeweiser ein, die von der Bibliothek GeoProver aus dem \textsc{SymbolicData}-Projekt abgeleitet wurde, und zeigen an einem Beispiel, wie man sie benutzt.
\\
Anschlie{\ss}end wird allgemein die {\"U}bersetzung von geometrischen Eigenschaften in Polynomideale behandelt. Dann kommen wir
zur Umsetzung des Ganzen in \ma: Dort werden als erstes die Konstruktoren zur Erzeugung eines Objektes in \ma\
beschrieben, dann
%Als erstes beschreiben wir die Konstruktoren zur Erzeugung eines Objektes in \ma, dann
definieren wir verschiedene Hilfsfunktionen, um mit ihrer Unterst{\"u}tzung die Funktionen zur {\"U}bersetzung zu beschreiben.
Das Kapitel endet mit drei Funktionen, die uns die Verwaltung der Polynome und die Anwendung des
\anf{Ideal-Membership-Test} erleichtern.

Im dritten Kapitel beweisen wir geometrische S{\"a}tze. Wir verwenden unser Beispiel aus dem vorherigen Kapitel erneut,
beweisen jedoch die Aussage jetzt automatisch. Beim zweiten Satz, dem Satz von Morley, gelingt es nicht, ihn direkt zu
beweisen; daher m{\"u}ssen wir erst eine Erweiterung des Satzes formulieren, um ihn beweisen zu k{\"o}nnen. Des Weiteren
beweisen wir die S{\"a}tze {\"u}ber den Feuerbachkreis, die Eulergerade, die Napoleonpunkte, die Pascalgerade und den
Exeterpunkt. Den Schluss der Arbeit bildet ein kleiner Benchmarktest von Computeralgebrasystemen.

S{\"a}mtliche zugeh{\"o}rigen Zeichnungen, Quelltexte und Links finden sich im Internet unter \urlvm{http://vm4.de/diplom} und
auf der beiliegenden CD.
\end{chapter}
