Einige computererzeugte Beweise

Mit ein paar Hilfsmittel, das sind Grassmann-Plücker-Relationen und Determinanten, ist es möglich einige Beweise geometrischer Sätze zu automatisieren, d.h. diese vom Computer finden zu lassen. Wie man dafür vorgehen kann wird anhand der beiden folgenden Beispielen veranschaulicht.

Der Satz von Desargues

Für den Satz von Desargues benötigen wir die zehn Punkte $0,\ldots, 9$ und gewissen Kollinearitäten wie sie unten im Applet gezeigt werden. Eine davon ist die Kollinearität der Punkte $1,2,3$. Nun kommen die beiden Hilfsmittel ins Spiel. Zuerst einmal wisse wir, dass die Determinanten $[123]$ der Punkte $1,2,3$ verschwindet, da diese kollinear sind. Des Weiteren gilt die Grassmann-Plücker-Relation

\[ [123] [145] - [124] [135] + [125] [134] = 0 \]

für beliebige Punkte $1,\ldots, 5$. Zusammen mit der Kollinearität von $1,2,3$ erhalten wir die Gleichung

\[ [125] [134] = [124] [135] \]

Die Bedingung, dass die Konstruktion nicht degeneriert sein soll, liefert, dass die Determinanten der eben hergeleiteten Gleichung nicht verschwinden. Das ergibt die erste Zeile der nachstehenden Auflistung. Fährt man analog fort für die weiteren Kollinearitäten, die für den Satz vorausgesetzt werden, so ergibt die folgende Aufstellung:

\[\begin{array}{ccc}(1,2,3)&\implies&[125][134] = [124][135]\\(1,4,0)&\implies&[148][103] = [143][108]\\(1,5,9)&\implies&[156][192] = [152][196]\\(4,2,8)&\implies&[421][487] = [427][481]\\(9,2,6)&\implies&[924][961] = [921][964]\\(0,8,3)&\implies&[081][035] = [085][031]\\(4,7,9)&\implies&[472][496] = [476][492]\\(5,3,6)&\implies&[531][567] = [537][561]\\(5,7,0)&\implies&[573][508] = [578][503] \end{array}\]

Multiplizieren wir jeweils die linken und rechten Seiten der Gleichungen und Kürzen entsprechend, so erhalten wir die Bedingung

\[ [764][785] = [765][784]. \]

Diese können wir wieder als Teil der Grassmann-Plücker-Relation

\[ [768] [745] - [765] [784] + [764] [785] = 0 \]

deuten, was soviel heißt, dass entweder $[768]$ oder $[745]$ verschwinden muss. Aufgrund der nicht-Degeneriertheit der Konstruktion muss $[768]=0$ gelten, was den Satz zeigt.

Satz von Pascal

Vollkommen analog kann man einen Beweis für den Satz von Pascal angeben, das einzige was man zusätzlich benötigt, ist ein Determinantenkriterium, das einem kodiert, dass sechs Punkte auf einem Kegelschnitt liegen. Aber das ist nicht schwer herzuleiten. Das entsprechenden Tableau für den Beweis ist das Folgende:

\[ \begin{array}{ccc} \bf{conic:} &\implies&[125][136][246][345]&=&[126][135][245][346]\\(1,5,9)& \implies&[517][592]&=&[512][597]\\(1,6,8)& \implies&[612][683]&=&[613][628]\\(2,4,9)& \implies&[245][297]&=&[247][295]\\(2,6,7)& \implies&[247][286]&=&[246][287]\\(3,4,8)& \implies&[346][385]&=&[345][386]\\(3,5,7)& \implies&[513][587]&=&[517][583]\\\\(9,8,7)&\Longleftarrow &[728][759]&=&[729][758]\\\end{array} \]

Automatisieren

Das Auffinden der eben beschriebenen Beweise lässt sich auf relativ einfache Weise automatisieren. Man erzeugt zunächst für die Hypothesen des Satzes alle mögliche Ausdrücke der Form $[abx][acy] = [aby][acx]$, die unter Annahme der Hypothesen automatisch gelten müssen ($a$, $b$, $c$) kommen hierbei von einem Tripel und $x$, $y$ sind beliebige andere Punkte der Konfiguration). Danach überprüft man, ob sich eine Teilmenge dieser Gleichungen so kombinieren lässt, dass durch Herauskürzen der auf linken und rechten Seiten auftauchenden Determinanten ein Fragment einer Grassmann-Plücker-Relation entsteht, aus dem man die Konklusion folgern kann.