\NewSession

Jetzt kommen wir zu dem eigentlichen Verfahren des automatischen Beweisens. Wir werden einen Algorithmus kennen lernen,
der Beziehungen zwischen Objekten der ebenen euklidischen Geometrie beweist. Wir legen kartesische Koordinaten in der
Euklidischen Ebene zugrunde. So entwickeln wir die Grundidee, dass sich eine gro{\ss}e Klasse von Voraussetzungen und Folgerungen
geometrischer S{\"a}tze als Polynomgleichungen zwischen den Koordinaten einer Punktmenge ausdr{\"u}cken l{\"a}sst.

Dieses Verfahren soll zun{\"a}chst an einem Beispiel veranschaulicht werden.
\begin{satz}\label{Satz Parallelogramm}
Es seien A, B, C, D die Ecken eines Parallelogramms in der Ebene, wie in der Abbildung \ref{Abb. Beispiel Parallelogramm} zu sehen. Die
Diagonalen $\overline{AD}$ und $\overline{BC}$ schneiden sich im Punkt $N$.

Die Strecken ($\overline{AN}$ und $\overline{ND}$) und ($\overline{BN}$ und $\overline{NC}$) sind
gleich lang, d.h. $\abs{AN}=\abs{DN}$ und $\abs{BN}=\abs{CN}$.
\end{satz}
In diesem Satz sind die Voraussetzungen von den Folgerungen durch einen Absatz, getrennt, um zu zeigen, wie der Satz aufgeteilt ist.
Im folgenden spielt die Unterscheidung zwischen Voraussetzung und Folgerung n{\"a}mlich eine wichtige Rolle.

\begin{figure}[h]
\begin{picture}(12,5)
\put(0,0){$A(0,0)$}
\put(0,0.5){\line(3,4){3}}
\put(3,4.8){$C(u_2,u_3)$}
\put(3,4.5){\line(1,0){7}}
\put(10,4.8){$D(x_1,x_2)$}
\put(7,0.5){\line(3,4){3}}
\put(0,0.5){\line(1,0){7}}
\put(7,0){$B(u_1,0)$}
%Diagonalen
\put(0,0.5){\line(5,2){10}}
\put(3,4.5){\line(1,-1){4}}
\put(5.5,2.35){$N(x_3,x_4)$}
\end{picture}
\caption{Parallelogramm}\label{Abb. Beispiel Parallelogramm}
\end{figure}

Als erstes k{\"o}nnen wir einige Vereinfachungen gegen{\"u}ber dem beliebigen Parallelogramm vornehmen und damit die zu
untersuchenden Voraussetzungen bzw. Folgerungen vereinfachen. Die Proportionen {\"a}ndern sich nicht unter Drehung oder
Verschiebung in der Ebene. Daher setzen wir in jedem weiteren Problem einen Punkt auf $(0,0)$. Dabei ist meist bereits
durch die normale geometrische Ansicht klar, welcher Punkt sich am besten eignet. Als zweite Vereinfachung k{\"o}nnen wir
die geometrischen Objekte drehen, so dass eine weitere Koordinate null wird.

Die unabh{\"a}ngigen Punkte in einem geometrischen Satz sind diejenigen, die beliebig gew{\"a}hlt werden k{\"o}nnen. Diese Wahl ist
allerdings nicht eindeutig, d.h. es gibt viele M{\"o}glichkeiten der Wahl der unabh{\"a}ngigen Punkte. Die abh{\"a}ngigen Punkte
hingegen richten sich nach den unabh{\"a}ngigen, liegen also aufgrund der Positionen der unabh{\"a}ngigen fest. Wir m{\"u}ssen an
dieser Stelle noch etwas feiner unterscheiden: Da wir zu jedem Punkt zwei Koordinaten haben, sprechen wir von
abh{\"a}ngigen bzw. unabh{\"a}ngigen Koordinaten. Wenn beide Koordinaten eines Punktes abh{\"a}ngig (unabh{\"a}ngig) sind, sprechen wir
weiterhin von abh{\"a}ngigen (unabh{\"a}ngigen) Punkten. Die unabh{\"a}ngigen Koordinaten bezeichnen wir im weiteren stets mit
$u_i$, die abh{\"a}ngigen mit $x_i$. Es sei im folgenden stets:\\
$\overline{u}=u_1,...,u_m$ die Menge der unabh{\"a}ngigen Koordinaten\\
und $\overline{x}=x_1,...,x_n$ die Menge der abh{\"a}ngigen Koordinaten.

\begin{bemerkung}[Wahl anderer unabh{\"a}ngiger Punkte]
Wie man sieht, wurden in Abbildung \ref{Abb. Beispiel Parallelogramm} $B, C$ als unabh{\"a}ngige Punkte gew{\"a}hlt und $D, N$ waren
daher abh{\"a}ngig. Man kann aber auch andere Punkte als unabh{\"a}ngig w{\"a}hlen:

\begin{figure}[h]
\begin{picture}(12,5)
\put(0,0){$A(0,0)$}
\put(0,0.5){\line(3,4){3}}
\put(3,4.8){$C(x_1,x_2)$}
\put(3,4.5){\line(1,0){7}}
\put(10,4.8){$D(u_2,u_3)$}
\put(7,0.5){\line(3,4){3}}
\put(0,0.5){\line(1,0){7}}
\put(7,0){$B(u_1,0)$}
%Diagonalen
\put(0,0.5){\line(5,2){10}}
\put(3,4.5){\line(1,-1){4}}
\put(5.5,2.35){$N(x_3,x_4)$}
\end{picture}
\caption{Parallelogramm mit anderen unabh{\"a}ngigen Punkten} \label{Beispiel Parallelogramm (andere Punkte)}
\end{figure}
Hier w{\"a}hlen wir $B,D$ als unabh{\"a}ngige Punkte. Das Parallelogramm ist durch $A, B, D$ definiert. Die Wahl der
unabh{\"a}ngigen Punkte kann die Gleichungen bzw. deren Aufstellung erheblich vereinfachen.
\end{bemerkung}

Wie wir jetzt schon gesehen haben, ist nicht eindeutig vorgegeben, welche Punkte unabh{\"a}ngig sind und welche nicht.
Wichtig -- f{\"u}r unsere Anwendung -- ist nur, dass wir die Punkte in unabh{\"a}ngige und abh{\"a}ngige trennen.

Im weiteren benutzen wir in diesem Beispiel das Parallelogramm aus Abbildung \ref{Abb. Beispiel Parallelogramm} mit den
dortigen $u_i$ und $x_i$.

Als n{\"a}chstes wollen wir unseren geometrischen Satz in seine Bestandteile zerlegen.\\
Parallelit{\"a}t der Seiten:
\begin{align}
\overline{AB}&\parallel\overline{CD}\label{AB parallel CD}\\
\notag &und\\
\overline{AC}&\parallel\overline{BD}\label{AC parallel BD}
\end{align}
Kollinearit{\"a}t:
\begin{align}
N&\text{ kollinear zu }A,D\label{N kollinear AD}\\
\notag &und\\
N&\text{ kollinear zu }B,C\label{N kollinear BC}.
\end{align}
Die Folgerung:
\begin{align}
\absover{AN}^2&=\absover{ND}^2\label{AN=ND}\\
\notag &und\\
\absover{BN}^2&=\absover{NC}^2\label{BN=NC}.
\end{align}

Jetzt {\"u}berf{\"u}hren wir die einzelnen Eigenschaften in Polynomgleichungen, dann diese in Variet{\"a}ten. Dazu schreiben wir
die geometrischen Eigenschaften als Polynome in den $u_i$ und $x_i$. Sodann konstruieren wir aus Eigenschaft \eqref{AC
parallel BD} eine Variet{\"a}t.Wir benutzen nicht Eigenschaft \eqref{AB parallel CD}, da sie sehr einfach ist und deshalb
kein gutes Beispiel abgibt. Die Parallelit{\"a}t beschreiben wir am einfachsten, indem wir sie durch gleiche Steigungen
ausdr{\"u}cken. Die Steigung von $\overline{AC}$ ist $\frac{u_3}{u_2}$ und die Steigung von $\overline{BD}$ ist
$\frac{x_2}{x_1-u_1}$, dabei ber{\"u}cksichtigen wir nicht die degenerierten F{\"a}lle $u_2=0$ und $x_1-u_1=0$. Daraus folgt
$\frac{u_3}{u_2}=\frac{x_2}{x_1-u_1}$. Nachdem wir die Nenner durch Multiplikation mit dem Hauptnenner entfernt haben, ergibt sich $(x_1-u_1)u_3-x_2u_2=0$ als
Gleichung. Die zugeh{\"o}rige Variet{\"a}t ist
\begin{equation*}
\Vfunc((x_1-u_1)u_3-x_2u_2).
\end{equation*}
Jeder Punkt dieser Variet{\"a}t definiert parallele Geraden $\overline{AC}$ und $\overline{BD}$.

Dieses Verfahren wenden wir auch f{\"u}r die anderen Bestandteile des Satzes an und erhalten folgende Gleichungen:

Die Parallelit{\"a}t von $\overline{AB}$ und $\overline{CD}$ (aus Gleichung \eqref{AB parallel CD}) liefert analog:
\begin{equation}
h_1=x_2-u_3=0\label{h1}.
\end{equation}
Die Parallelit{\"a}t von $\overline{AC}$ und $\overline{BD}$ (aus Gleichung \eqref{AC parallel BD}) impliziert, wie gesehen:
\begin{equation}
h_2=(x_1-u_1)u_3-x_2u_2=0\label{h2}.
\end{equation}
Kollinearit{\"a}t von $N,A$ und $D$ (aus Gleichung \eqref{N kollinear AD}) beschreibt man durch
\begin{equation}
\frac{x_4}{x_3}=\frac{u_3}{x_1}\overset{\text{\anf{Nenner entfernen}}}{\Longrightarrow} h_3=x_4x_1-x_3u_3=0\label{h3},
\end{equation}
und die Kollinearit{\"a}t von $N,B$ und $C$ (aus Gleichung \eqref{N kollinear BC}) durch
\begin{equation}
h_4=x_4(u_2-u_1)-(x_3-u_1)u_3=0\label{h4}.
\end{equation}
Die Folgerung $\absover{AN}^2=\absover{ND}^2$ (aus Gleichung \eqref{AN=ND}) ist {\"a}quivalent zur Richtigkeit folgender
Gleichung:
\begin{equation}
x_3^2+x_4^2=(x_3-x_1)^2+(x_4-x_2)^2\Leftrightarrow g_1=x_1^2-2x_1x_3-2x_4x_2+x_2^2=0\label{g1}.
\end{equation}
Analog l{\"a}sst sich die zweite Folgerung $\absover{AN}^2=\absover{ND}^2$  (aus Gleichung \eqref{BN=NC}) als
\begin{equation}
g_2=2x_3u_1-2x_3u_2-2x_4u_3-u_1^2+u_2^2+u_3^2=0\label{g2}
\end{equation}
schreiben.

Als {\"U}bersetzungen der Voraussetzungen zu diesem Beispiel verwenden wir die Gleichungen \eqref{h1}, \eqref{h2},
\eqref{h3} und \eqref{h4}:
\begin{align*}\label{Uebersetzung der Vor}
h_1&=x_2-u_3=0\\
h_2&=(x_1-u_1)u_3-x_2u_2=0\\
h_3&=x_4x_1-x_3u_3=0\\
h_4&=x_4(u_2-u_1)-(x_3-u_1)u_3=0.
\end{align*}
In diesem Beispiel beweisen wir nur die erste Folgerung (Gleichung \eqref{g1}), die zweite funktioniert dann analog.

Um zu beweisen, dass aus den Voraussetzungen \eqref{h1}-\eqref{h4} die Folgerung \eqref{g1} resultiert, ist zu
{\"u}berpr{\"u}fen, ob $\Vfunc(g_1)$ die Variet{\"a}t $\Vfunc(h_1,\ldots,h_4)$ umfasst. Damit w{\"a}re gezeigt, dass f{\"u}r Punkte, die
$h_1=0,\ldots, h_4=0$ erf{\"u}llen, auch $g_1=0$ gilt. Dazu gehen wir zu den Verschwindungsidealen {\"u}ber:

$\sqrt{g_1}\subset\Ifunc(\Vfunc(h_1,\ldots,h_4))$ ist {\"a}quivalent (nach HNS \ref{Hilbertscher Nullstellensatz}) zu $g_1\in\sqrt{\langle h_1,\ldots,h_4\rangle}$.

Um dies zu {\"u}berpr{\"u}fen, wenden wir den Ideal-Membership-Test (aus \ref{Korollar zur generalisierten Folgerung}) an. Dazu berechnen wir eine
{\gb} von
\begin{equation}\label{Ideal Membership Test die Erste}
\overline{I}=\langle h_1,h_2,h_3,h_4,1-y g_1\rangle\in\rmenge[u_1,u_2,u_3,x_1,x_2,x_3,x_4,y].
\end{equation}
Wenn die {\gb} gleich $\{1\}$ ist, wissen wir nach Satz \ref{Radical Membership}, dass $\overline{I}=\rmenge[u_1,u_2,u_3,x_1,x_2,x_3,x_4,y]$,
und damit liegt $g_1$ in $\sqrt{\langle h_1,\ldots,h_4\rangle}$.

In \ma\ f{\"u}hren wir dazu folgende Berechnung aus: \dispTFinmath{ \MathBegin{MathArray}{l}
\Mvariable{h1}=\Mvariable{x2}-\Mvariable{u3};  \\
\noalign{\vspace{0.625ex}}  \\
\Mvariable{h2}=(\Mvariable{x1}-\Mvariable{u1})\Mvariable{u3}-\Mvariable{u2}\multsp \Mvariable{x2};  \\
\noalign{\vspace{0.625ex}}  \\
\Mvariable{h3}=\Mvariable{x4}\multsp \Mvariable{x1}-\Mvariable{x3}\multsp \Mvariable{u3};  \\
\noalign{\vspace{0.625ex}}  \\
\Mvariable{h4}=\Mvariable{x4}(\Mvariable{u2}-\Mvariable{u1})-(\Mvariable{x3}-\Mvariable{u1})\Mvariable{u3};  \\
\noalign{\vspace{0.625ex}}  \\
g=\Mvariable{x1}\RawWedge 2-2\Mvariable{x1}\multsp \Mvariable{x3}-2\Mvariable{x4}\multsp \Mvariable{x2}+\Mvariable{x2}\RawWedge 2;  \\
\noalign{\vspace{0.625ex}}  \\
\Mfunction{GroebnerBasis}[\{\Mvariable{h1},\Mvariable{h2},\Mvariable{h3},\Mvariable{h4},1-y\multsp g\},\{\Mvariable{u1},\Mvariable{u2},\Mvariable{u3},\Mvariable{x1},\Mvariable{x2},\Mvariable{x3},\Mvariable{x4},y\}]
\MathEnd{MathArray}
}

\dispTFoutmath{
\MathBegin{MathArray}{l}
\{-2\multsp \Mvariable{x2}\multsp y\multsp {{\Mvariable{x4}}^3}+{{\Mvariable{x2}}^2}\multsp y\multsp {{\Mvariable{x4}}^2}-{{\Mvariable{x4}}^2}-2\multsp
\Mvariable{x2}\multsp {{\Mvariable{x3}}^2}\multsp y\multsp \Mvariable{x4}+{{\Mvariable{x2}}^2}\multsp {{\Mvariable{x3}}^2}\multsp y,  \\
\noalign{\vspace{0.601563ex}}
\hspace{1.em} \Mvariable{x2}\multsp \Mvariable{x3}-\Mvariable{x1}\multsp \Mvariable{x4},\Mvariable{x4}\multsp y\multsp {{\Mvariable{x2}}^2}-2\multsp
{{\Mvariable{x3}}^2}\multsp y\multsp \Mvariable{x2}-2\multsp {{\Mvariable{x4}}^2}\multsp y\multsp \Mvariable{x2}+\Mvariable{x1}\multsp \Mvariable{x3}\multsp
y\multsp \Mvariable{x2}-\Mvariable{x4},  \\
\noalign{\vspace{0.601563ex}}
\hspace{1.em} -y\multsp {{\Mvariable{x1}}^2}+2\multsp \Mvariable{x3}\multsp y\multsp \Mvariable{x1}-{{\Mvariable{x2}}^2}\multsp y+2\multsp \Mvariable{x2}\multsp
\Mvariable{x4}\multsp y+1,\Mvariable{x2}-\Mvariable{u3},\Mvariable{x2}\multsp \Mvariable{x3}-\Mvariable{u2}\multsp \Mvariable{x4},\Mvariable{x1}\multsp
\Mvariable{x2}-\Mvariable{u2}\multsp \Mvariable{x2},\Mvariable{u1}\multsp \Mvariable{x4},\Mvariable{u1}\multsp \Mvariable{x2}\}\\
\MathEnd{MathArray} } Leider ist die {\gb} nicht $\{1\}$. Sonst h{\"a}tten wir den Beweis bereits zu Ende gef{\"u}hrt. Da es
sich um einen wahren geometrischen Satz handelt, m{\"u}ssen wir versuchen zu verstehen, warum der Beweis nicht zum Ziel
f{\"u}hrt. Dazu berechnen wir als erstes die {\gb} von $I=\langle h_1,h_2,h_3,h_4\rangle$:

\dispTFinmath{
\MathBegin{MathArray}{l}
\{\Mfunction{GroebnerBasis}[\{\Mvariable{h1},\Mvariable{h2},\Mvariable{h3},\Mvariable{h4}\},\{\Mvariable{x1},\Mvariable{x2},\Mvariable{x3},\Mvariable{x4},\Mvariable{u1},\Mvariable{u2},\Mvariable{u3}\}]\}
\MathEnd{MathArray}
}

\dispTFoutmath{
\left(\NoBreak \MathBegin{MathArray}[c]{c}
    -\Mvariable{u1}\multsp \Mvariable{u3}\multsp (\Mvariable{u3}-2\multsp \Mvariable{x4}) \\
    -\Mvariable{u1}\multsp (\Mvariable{u1}-\Mvariable{u2})\multsp (\Mvariable{u3}-2\multsp \Mvariable{x4}) \\
    \Mvariable{u1}\multsp \Mvariable{u3}-\Mvariable{x3}\multsp \Mvariable{u3}-\Mvariable{u1}\multsp \Mvariable{x4}+\Mvariable{u2}\multsp \Mvariable{x4}
\\
    \Mvariable{x2}-\Mvariable{u3} \\
    -\Mvariable{u3}\multsp (\Mvariable{u1}+\Mvariable{u2}-\Mvariable{x1}) \\
    \Mvariable{u1}\multsp \Mvariable{u3}-\Mvariable{u1}\multsp \Mvariable{x4}+\Mvariable{u2}\multsp \Mvariable{x4}-\Mvariable{x1}\multsp \Mvariable{x4}

  \MathEnd{MathArray}\NoBreak \right)
}
\begin{equation*}%\label{Faktoren bestimmen}
\begin{split}
f_1&=u_1u_3(2x_4-u_3)\\
f_2&=u_1(u_1-u_2)(2x_4-u_3)\\
f_3&=u_1u_3-x_3u_3-u_1x_4+u_2x_4\\
f_4&=x_2-u_3\\
f_5&=u_3(x_1-u_1-u_2)\\
f_6&=u_1u_3-u_1x_4+u_2x_4-x_1x_4.
\end{split}
\end{equation*}

Die {\gb} ist reduzibel, da $f_5$ in zwei Faktoren zerf{\"a}llt, $x_1-u_1-u_2$ und $u_3$. Daraus folgt, dass wir die
Variet{\"a}t zerlegen k{\"o}nnen:
\begin{equation*}%\label{Varietaet f_5 zerlegen}
\begin{split}
V_1&=\Vfunc(f_1,f_2,f_3,f_4,x_1-u_1-u_2,f_6)\\
V_2&=\Vfunc(f_1,f_2,f_3,f_4,u_3,f_6)\\
V_p&=V_1\cup V_2.
\end{split}
\end{equation*}
Jetzt berechnen wir eine {\gb} f{\"u}r $V_1$, dabei ergibt sich:
\begin{equation*}%\label{\gb zu V_1 berechnen}
\begin{split}
p_1&=u_1(u_3-2x_4)\\
p_2&=2x_3u_3-2u_2x_4-u_1u_3\\
p_3&=x_2-u_3\\
p_4&=x_1-u_1-u_2,
\end{split}
\end{equation*}
wobei $p_1,\ldots,p_n$ die Polynome der \gb\ von $V_1$ sind. Da $p_1$ ebenfalls in Faktoren zerf{\"a}llt, k{\"o}nnen wir mit
der Zerlegung fortfahren und erhalten:
\begin{align*}%\label{Zerlegung Fortsetzung}
V_{1_1}&=\Vfunc(u_1,p_2,p_3,p_4)\\
V_{1_2}&=\Vfunc(u_3-2x_4,p_2,p_3,p_4)\\
V_1&=V_{1_1}\cup V_{1_2}. \intertext{So setzen wir die Berechnungen fort, indem wir die {\gbn} f{\"u}r $V_{1_1}$ und
$V_{1_2}$ berechnen, und diese Zerlegung fortsetzen, bis keine Faktoren mehr auftreten. Dies f{\"u}hrt zu:}
V_{1_1}&=\Vfunc(u_1,u_3x_3-u_2x_4,x_2-u_3,x_1-u_2)\\
V_{1_2}&=\Vfunc(u_3-2x_4,u_3(u_1+u_2-2x_3),x_2-u_3,x_1-u_1-u_2)\\
V_{2_1}&=\Vfunc(u_3,x_4,x_2)\\
V_{2_2}&=\Vfunc(u_3,u_1-u_2,x_2,x_1x_4).\\
\intertext{Hier sind nur noch $V_{1_2}$ und $V_{2_2}$ zerlegbar, und dabei sehen wir sofort, dass gilt:}
V_{2_{2_1}}&=\Vfunc(u_3,u_1-u_2,x_2,x_1)\\
V_{2_{2_2}}&=\Vfunc(u_3,u_1-u_2,x_2,x_4).
\intertext{Mittels {\gbn} berechnen wir zus{\"a}tzlich die Zerlegung von $V_{1_2}$:}
V_{1_{2_1}}&=\Vfunc(u_3-2x_4,u_3,x_2-u_3,x_1-u_1-u_2)\\
V_{1_{2_2}}&=\Vfunc(u_3-2x_4,u_1+u_2-2x_3,x_2-u_3,x_1-u_1-u_2).
\end{align*}
Damit ergibt sich f{\"u}r $V_p$ folgende Zerlegung in irreduzible Variet{\"a}ten
\begin{equation*}%\label{Zusammensetzen der Varietaet}
V_p=V_{1_1}\cup V_{1_{2_1}}\cup V_{1_{2_2}}\cup V_{2_1}\cup V_{2_{2_1}}\cup V_{2_{2_2}}.
\end{equation*}

Als n{\"a}chstes streichen wir $V_{1_{2_1}}$ und $V_{2_{2_2}}$, da sie beide in $V_{2_1}$ enthalten sind. Jetzt haben wir
eine irreduzible Zerlegung von $V_p$:
\begin{equation*}%\label{Zusammensetzen der Varietaet ohne gleiche}
V_p=V_{1_1}\cup V_{1_{2_2}}\cup V_{2_1}\cup V_{2_{2_1}}.
\end{equation*}

Betrachten wir nun die Variet{\"a}ten aus geometrischer Sicht. Zur {\"U}bersichtlichkeit bilden wir hier noch einmal das
Parallelogramm ab:
\begin{figure}[ht]
\begin{picture}(12,5)
\put(0,0){$A(0,0)$}
\put(0,0.5){\line(3,4){3}}
\put(3,4.8){$C(u_2,u_3)$}
\put(3,4.5){\line(1,0){7}}
\put(10,4.8){$D(x_1,x_2)$}
\put(7,0.5){\line(3,4){3}}
\put(0,0.5){\line(1,0){7}}
\put(7,0){$B(u_1,0)$}
%Diagonalen
\put(0,0.5){\line(5,2){10}}
\put(3,4.5){\line(1,-1){4}}
\put(5.5,2.35){$N(x_3,x_4)$}
\end{picture}
\caption{Parallelogramm}
\end{figure}
\begin{enumerate}
\item Bei $V_{1_1}$ gilt $u_1=0$; daraus folgt, dass die Grundlinie des Parallelogramms die L{\"a}nge null hat, dies ist
ein degenerierter Fall. \item Im Fall $V_{1_{2_2}}$ haben wir:
\begin{equation*}%\label{Die Varietaet zum Parallelogramm}
V_{1_{2_2}}=\Vfunc(u_3-2x_4,u_1+u_2-2x_3,x_2-u_3,x_1-u_1-u_2).
\end{equation*}
Dies ist kein degenerierter Fall, da kein Polynom der Variet{\"a}t aus $\rmenge[\overline{u}]$ ist, d.h. die Variet{\"a}t ist algebraisch unabh{\"a}ngig von $\overline{u}$.
\item Bei $V_{2_1}$ gilt $u_3=0$, hier ist dann die H{\"o}he null $\Rightarrow$ degenerierter Fall.
\item Ebenso bei $V_{2_{2_1}}$ gilt $u_3=0$ $\Rightarrow$ degenerierter Fall.
\end{enumerate}

Lassen wir nun die degenerierten F{\"a}lle weg, dann erhalten wir als Variet{\"a}t f{\"u}r die Voraussetzung:
\begin{equation*}%\label{Die Varietaet zum Parallelogramm die zweite}
V_p=V_{1_{2_2}}.
\end{equation*}

{\"U}berpr{\"u}fen wir nun, ob die Folgerung $g_1$ auf $V_p$ verschwindet. Dazu berechnen wir die {\gb} von
$\{u_3-2x_4,u_1+u_2-2x_3,x_2-u_3,x_1-u_1-u_2,\bf{1-yg_1}\}$: \dispTFinmath{
\Mfunction{GroebnerBasis}[\{\Mvariable{v122},1-y\multsp
\Mvariable{g1}\},\{\Mvariable{u1},\Mvariable{u2},\Mvariable{u3},\Mvariable{x1},\Mvariable{x2},\Mvariable{x3},\Mvariable{x4}\}]
}

\dispTFoutmath{ \{1\} }

nun gilt $g_1\in\sqrt{V_p}$, d.h. unser geometrischer Satz ist bewiesen. Wir haben viele F{\"a}lle auf unserem Weg hierher
ausgeschlossen, um genau zu sein
%Betrachten wir nun einen dieser F{\"a}lle, um zu zeigen, dass das Wort \anf{degeneriert} f{\"u}r diese F{\"a}lle begr{\"u}ndet ist.
%Wir verwenden hierzu eine der Variet{\"a}ten aus unserer Zerlegung, $V_{2_1}=\Vfunc(u_3,x_4,x_2)$.
%Die geometrischen Auswirkungen auf das Parallelogramm haben wir bereits oben gesehen.
%{\"u}berlegen uns die geometrischen Auswirkungen auf unser Parallelogramm. Die Variablen $u_3,x_4,x_2$ sind $0$, daher
%liegen die Punkte $C,D$ und $N$ auf der $x$-Achse, d.h. das Parallelogramm hat die H{\"o}he $0$. Dies ist ein degenerierter
%Fall, denn es liegt kein Parallelogramm vor.
%
%So oder {\"a}hnlich verhalten sich
%alle degenerierten F{\"a}lle, denn wenn wir ein Polynom in $\rmenge[\overline{u}]$ verwenden, welches verschwindet, bedeutet das, dass die unabh{\"a}ngigen Punkte
%voneinander abh{\"a}ngen.
alle die Polynome in $\rmenge[\overline{u}]$ enthalten, weil bei diesen F{\"a}llen unsere unabh{\"a}ngigen Koordinaten $u_i$ voneinander abh{\"a}ngen.
%Diese Auswahl haben wir bisher nicht automatisch getroffen.
Um den Weg zur{\"u}ck zum \anf{automatischen} Beweisen zu finden, m{\"u}ssen wir diese Schritte automatisieren.
%Dazu verwenden wir den Satz \ref{Satz zur generalisierten Folgerung}, der es uns erlaubt, degenerierte F{\"a}lle zu erkennen.

%Zerlegen wir nun die Variet{\"a}t $V$ in endlich viele, disjunkte, irreduzible Variet{\"a}ten (gem{\"a}{\ss} Satz \ref{Zerlegung von Varietaeten in irreduzible}):
%\begin{equation*}%\label{Zerlegung von V}
%V=V_1\cup \ldots \cup V_k.
%\end{equation*}

Mithilfe von Korollar \ref{Korollar zur generalisierten Folgerung} (ii) haben wir eine M{\"o}glichkeit, automatisch zu pr{\"u}fen, ob eine Folgerung generalisiert aus den Voraussetzungen folgt.
Dazu berechnen wir eine {\gb} {\"u}ber $\rmenge[x_1,...,x_n]$ mit Koeffizienten aus $\rmenge(u_1,\ldots,u_m)$.
Ein Beispiel dazu werden wir in Abschnitt \ref{Uebersetzung der Geometrie in Polynome am Beispiel} sehen.

Mit diesem Resultat gehen wir zur Umsetzung in \ma\ {\"u}ber.
