BannerBannerBanner

Automatisches Beweisen


Beweisverfahren

Das automatische Beweisen geometrischer Sätze befasst sich mit der Frage, wie man aus der kombinatorischen Struktur einer geometrischen Konstruktion direkt einen Beweis herleiten kann. Man unterscheidet dabei im Wesentlichen Logik basierte, algebraische und randomisierte Beweisverfahren.

Bitte schalten Sie Java ein, um eine Cinderella-Konstruktion zu sehen.
[JAE][JHD][IDA][IHE] = [IHD][IAE][JHE][JDA]
[IHD][JHG][JDC][ICG] = [JHD][IDC][IHG][JCG]
[JCG][ICB][FIG][FJB] = [ICG][JCB][FJG][FIB]
[IAE][JAB][FIB][FJE] = [JAE][IAB][FJB][FIE]
[JDA][IDC][IAB][JCB] = [IDA][JDC][JAB][ICB]
[JHE][IHG][FJG][FIE] = [IHE][JHG][FIG][FJE]
Ziehen sie an den hellroten Punkten
Das neben stehende Bild zeigt den Satz von Miquel und einen automatisch (!) erzeugten symbolischen Beweis. Der Satz besagt, dass wenn sechs Kreise die Inzidenzen an den Punkten A,B,C,D,E,F,H erfüllen, sich automatisch die drei roten Kreise in einem Punkt (hier G) schneiden. Der darunter notierte algebraische Beweis lässt sich folgendermassen verstehen. Jede Gleichung drückt die Kozirkularität von 4 Punkten aus. (Hier bei werden die Positionen der Punkte in dreidimensionalen homogenen Koordinaten kodiert. Die Punkte I und J haben die speziellen Koordinaten I=(1,i,0) und J=(-1,i,0), und der Ausdruck [A,B,C] steht für die 3x3 Determinante der homogenen Punktkoordinaten von A,B und C.) Betrachtet man nun die oberen fünf Gleichungen, multipliziert alle Ausdrücke auf den linken und rechten Seiten und kürzt Determinanten die auf beiden Seiten auftreten heraus, so ergibt sich genau die letzte Gleichung. Nutzt man, wie im nebenstehenden Beweis, invariantentheoretische Methoden aus, so kann man automatische Beweiser konstruieren, die gezielt kurze und lesbare Beweise finden, welche viel strukturelle Information über den zu beweisenden Satz enthalten. Beweise, die letzlich auf ein Kürzungsmuster der obigen Art zurückgeführt werden, nennt man binomiale Beweise. Sie spielen auch bei Nichtrealisierbarkeitsbeweisen der kombinatorischen Geometrie eine herausragende Rolle. Der Vorteil eines solchen Beweisers liegt darin, dass Beweise schnell gefunden werden können, kurz und lesbar sind. Der Nachteil besteht darin, dass beweisbar nicht alle geometrischen Theoreme damit bewiesen werden können. Das allgemeine Auffinden eines Beweises stellt sich tatsächlich als mindestens NP-schwer heraus, während binomiale Beweise in polynomieller Zeit gefunden werden können.

Beweiser in Cinderella

Ein solches Beweisverfahren war der Ausgangspunkt für das Projekt Cinderella, welches ursprünglich hauptsächlich als Eingabeinterface für den Beweiser dienen sollte. Aufgrund der Tatsache, dass keine Garantie für das Auffinden eines binomialen Beweises existiert, wurde allerdings mittlerweile der Cinderella interne Beweiser gegen ein randomisiertes Verfahren ausgetauscht. Ein randomisierter Beweiser erzeugt zwar keinen Beweis im klassischen Sinn, kann aber sofern ein Theorem vorliegt, mit extrem kleiner Irrtumswahrscheinlichkeit dessen Existenz nachweisen. Letztlich werden für einen vermuteten Satz viele zufällig generierte Instanzen getestet, wird kein Gegenbeispiel gefunden, so gibt das so genannte Schwartz/Zippel-Theorem eine exakte Schranke für die Irrtumswahrscheinlichkeit. Das Ausnutzen des automatischen Beweisers in Cinderella hat vielfältige Anwendungsfelder, angefangen vom automatischen Klassifizieren von Ortskurven, über das sauber Halten der interaktiven Datenstruktur, bis hin zu Schüleraufgaben mit automatischer Lernerfolgskontrolle.