Theorieexploration in Theorema: Neueste Ansätze zur Gröbner Basen Theorie

Computer-assistierte mathematische Theorieentwicklung hat in erster Linie die strukturierte Darstellung einer mathematischen Theorie in einem Softwaresystem zum Ziel. Dies soll, im Gegensatz zu Mathematik in Büchern, so geschehen, dass sowohl Mensch als auch Maschine (also Software) den Inhalt verstehen können. Verstehen bedeutet im Zusammenhang mit Software unter Anderem, dass diese aus bekannten Fakten neue Fakten ableiten kann und das vollkommen selbstständig. Dadurch werden Mathematiker, die neue Theorien basierend auf bereits bestehenden entwickeln wollen, von der Software unterstützt, und deshalb werden solche Softwaresysteme auch als mathematische Assistenzsysteme bezeichnet. Kurz und prägnant ausgedrückt geht es in der computer-assistierten Theorieentwicklung also darum, Computern Mathematik beizubringen (und zwar nicht nur das Rechnen, sondern vor Allem auch das logische Denken). Das Hauptziel dieses Projekts ist nun die formale Entwicklung einer bestimmten mathematischen Theorie im Theorema-Assistenzsystem. Die Theorie, um die es sich handelt, ist die Theorie der Gröbner Basen. Diese Theorie wurde 1965 von Bruno Buchberger, der auch das Theorema-Projekt initiiert hat und leitet, entwickelt und finden heutzutage in vielen naturwissenschaftlich-technischen Bereichen Anwendung, z.B. in der Robotik, Kryptographie, Optimierung, Thermodynamik, Computer-Aided Design, und vielen anderen Gebieten, in denen es um nicht-lineare Vorgänge geht. Das Hauptaugenmerk bei der Formalisierung der Theorie liegt auf einer Methode zur Berechnung von Gröbner Basen mithilfe von Matrizen, die erst vor Kurzem entwickelt wurde. Zuerst soll diese Methode formalisiert und implementiert werden, dann soll ihre Korrektheit unter Zuhilfenahme von Theorema bewiesen werden (die Zuhilfenahme von Theorema stellt sicher, dass jeder einzelne Beweisschritt logisch korrekt ist und keine falschen Schlussfolgerungen gemacht werden). Tatsächlich ist dies das erste Mal, dass genau dieser Teil der Gröbner Basen Theorie in einem mathematischen Assistenzsystem behandelt wird. Eine entscheidende Motivation für die Durchführung dieses Projekts ist die geplante Teilnahme am internationalen Global Digital Mathematics Library (GDML) Projekt, dessen ambitioniertes Ziel es ist, einen Großteil der gesamten existierenden Mathematik zu sammeln und in digitaler Form bereitzustellen, die sowohl von Menschen, als auch von Softwaresystemen verstanden werden kann. Buchberger ist ein Mitglied im achtköpfigen Steering Committee dieses globalen Mathematik-Projekt. Parallel zu den mathematischen Projekten im Rahmen von Theorema werden jetzt auch industrielle Anwendungen der "Automatisierung des mathematischen Denkens" im Bereich des semantischen Webs und zum automatischen Entwickeln von Software für Anwendungen der künstlichen Intelligenz verfolgt.

Das Hauptresultat dieses Projekts war die Erstellung einer formalen Bibliothek mathematischer Theorien, die sich mit sogenannten Gröbner Basen beschäftigen. Das bedeutet, dass wir bestehende Theorien, in Form von Büchern und Zeitschriftenartikeln, in eine formale Sprache übersetzt haben, die von einem Softwaresystem -- einem sogennanten Beweisassistenten -- verstanden wird. Dieses Softwaresystem -- in unserem Fall Isabelle/HOL -- überprüft dann jeden einzelnen Beweisschritt und bestätigt, dass er tatsächlich korrekt ist, und dass weiters keine Schritte fehlen. Somit kann die wissenschaftliche Gemeinschaft vollkommen auf die Richtigkeit solcherart formalisierter mathematischer Theorien vertrauen und sie als solide Basis für weitere Entwicklungen verwenden. In diesem Projekt war die mathematische Theorie, deren Formalisierung wir uns gewidment haben, die Theorie der Gröbner Basen. Erfunden 1965 von Bruno Buchberger, ist diese Theorie heutzutage eine der zentralen und am weitesten verbreiteten Theorien im Bereich der kommutativen Algebra. Interessanterweise jedoch wurden bisher nur vergleichsweise kleine Teile von ihr in Beweisassistenten formalisiert. Die Arbeit an diesem Forschungsprojekt ermöglichte es uns, das zu ändern; insbesondere haben wir uns dabei auf neue Ansätze zur Berechnung von Gröbner Basen mittels neuer, erst vor wenigen Jahren entwicklten Algorithm konzentriert. Einer dieser Ansätze besteht darin, die gegebenen Daten, d.h. eine Liste von Polynomen, in eine große Matrix zu transformieren (d.h. eine tabellarische Anordnung von Zahlen), dann eine Reihe bekannter Operationen auf diese Matrix anzuwenden, und schließlich das Ergebnis in den gewünschten Output zurück zu transformieren. Außerdem haben wir auch sogenannte signaturbasierte Algorithmen zur Berechnung von Gröbner Basen formalisiert. Diese Klasse von Algorithmen wurde 2001 entwickelt und erst 2012 als vollständig korrekt bewiesen. Sie stellt den aktuellen Stand der Technik in Berechnungen von Gröbner Basen dar, da sie jeden anderen bekannten Algorithmus in beinahe jeder konkreten Probleminstanz übertrifft. All diese Formalisierungen sind die ersten ihrer Art, und frei verfügbar für die Allgemeinheit. Sie stellen einen Mehrwert für die wissenschaftliche Gemeinschaft dar, da Forscher und andere auf diesem Gebiet Tätigen nun ihre eigenen Formalisierungen auf ihnen aufbauen können. Eine zweite wichtige Leistung dieses Projekts war die Entwicklung eines Add-on Pakets für den Open-Source Beweisassistenten Theorema, genannt Theorema-HOL. Theorema-HOL fügt dem System einige Features hinzu, die in Isabelle/HOL bereits vorhanden sind, in Standard-Theorema aber noch gefehlt haben. Unter anderem sind das eine Reihe von Beweismethoden zum automatischen Beweisen von Theoremen und ein flexibler, textbasierter interaktiver Beweismodus zum Beweisen schwierigerer Theoreme, die nicht automatisch bewiesen werden können. Der ursprüngliche Plan war, die oben genannten Theorien in Theorema-HOL zu formalisieren, aber leider mussten wir einstweilen zum besser ausgestatteten Isabelle/HOL System wechseln und die Formalisierung in Theorema-HOL auf ein potenzielles zukünftiges Projekt verschieben.