Zur Seitenansicht
 

Titelaufnahme

Titel
Computer-assisted exploration of Gröbner bases theory in Theorema / eingereicht von DI Alexander Maletzky
VerfasserMaletzky, Alexander
Begutachter / BegutachterinBuchberger, Bruno ; Kreuzer, Martin
ErschienenLinz, Mai 2016
Umfangx, 184 Seiten : Illustrationen
HochschulschriftUniversität Linz, Univ., Dissertation, 2016
Anmerkung
Zusammenfassung in deutscher Sprache
SpracheEnglisch
Bibl. ReferenzOeBB
DokumenttypDissertation
Schlagwörter (DE)Gröbner Basen / Computer-unterstützte Theorieexploration / automatisches Beweisen / Reduktionsringe / Theorema
Schlagwörter (EN)Gröbner bases / computer-assisted theory exploration / automated reasoning / reduction rings / Theorema
Schlagwörter (GND)Gröbner-Basis / Exploration / Computerunterstütztes Verfahren / Automatisches Beweisverfahren / Theorema
URNurn:nbn:at:at-ubl:1-10800 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist gemäß den "Hinweisen für BenützerInnen" verfügbar
Dateien
Computer-assisted exploration of Gröbner bases theory in Theorema [1.62 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Die vorliegende Dissertation präsentiert die formale, computerunterstützte Exploration der Theorie der Gröbner Basen im mathematischen Assistenzsystem Theorema 2.0. Die Hauptmotivation für diese Arbeit ist unsere Überzeugung, daßeine vollständig formale, verifizierte und sogar exekutierbare Darstellung der Theorie deren zukünftige Erweiterung deutlich vereinfachen kann. Den Kern der Formalisierung stellen sogenannte Reduktionsringe dar, die vor über 30 Jahren von Buchberger eingeführt wurden. Reduktionsringe verallgemeinern das ursprüngliche "Setting" von Gröbner Basen in Polynomringen über Körpern zu einer viel größeren Klasse algebraischer Strukturen, nämlich im Wesentlichen zu unitären kommutativen Ringen mit ein paar zusätzlichen Funktionen und Relationen, die eine Handvoll nicht-trivialer Axiome erfüllen. Wir haben alle zentralen Aspekte dieser Theorie in Theorema dargestellt, d.h. insbesondere alle wichtigen Definitionen und Sätze, und haben sämtliche Resultate mithilfe der automatischen und interaktiven Beweisfunktionen von Theorema bewiesen. Außerdem haben wir den Buchberger-Algorithmus zur Berechnung von Gröbner Basen in einer komplett generischen und direkt ausführbaren Weise implementiert und die totale Korrektheit dieser Implementierung bewiesen. Das Ergbnis von alledem ist nun als Sammlung von 16 Theorema-Theorien, bestehend aus insgesamt ca. 2240 Formeln, verfügbar, welche als Basis für zukünftige Theorieexplorationen in Theorema dienen kann. Obwohl die mathematischen Theorien, die wir formalisiert haben, keineswegs neu sind, konnten wir dennoch auch direkt zu ihnen beitragen, und zwar durch die drastische Verinfachung eines Beweises, die Verallgemeinerung von verschiedenen Definitionen und Resultaten, und, am allerwichtigsten, durch das Korrigieren eines kleinen Fehlers in der Reduktionsringtheorie. Das alles unterstützt definitiv die Behauptung, Mathematik würde davon profitieren, formal in einem Computersystem behandelt zu werden, und ist deshalb eine zusätzliche Motivation für unsere Arbeit im Speziellen und für computerunterstützte Theorieexploration im Allgemeinen. Schließlich berichtet die Dissertation auch über vier neue Werkzeuge in Theorema, die wir im Rahmen unserer Arbeit entwickelt haben: einen Rewriting-Mechanismus für Regeln erster- und höherer Ordnung, eine Sammlung von Inferenzregeln für allgemeine Prädikatenlogik, eine Beweisstrategie für interaktives Beweisen, und eine Sammlung von Funktionen zur Analyse der logischen Struktur von Theorema-Theorien. Jedes dieser Werkzeuge hat sich bereits als äußerst hilfreich in der Formalisierung der Gröbner Basen Theorie herausgestellt und wird deshalb sicherlich auch in zukünftigen Theorieexplorationen in Theorema Anwendung finden.

Zusammenfassung (Englisch)

This thesis presents the formal, computer-supported exploration of the theory of Gröbner bases in the mathematical assistant system Theorema 2.0. The main motivation for this work is our conviction that a fully formal, verified and even executable representation of the theory has the potential to facilitate its further expansion in the future. The core component of the computer-formalization are so-called reduction rings, introduced by Buchberger more than 30 years ago. Reduction rings generalize the original setting of Gröbner bases in polynomial rings over fields to a much wider class of algebraic structures, namely essentially commutative rings with multiplicative identity and a couple of further functions and relations, satisfying a handful of non-trivial axioms. We represented the central aspects of this theory in Theorema, including all the main definitions and theorems, and proved the results correct using the automated- and interactive proving facilities of Theorema. Moreover, we also implemented Buchberger's algorithm for actually computing Gröbner bases in a completely generic and directly executable manner and proved it totally correct. The result of all this is now available as a collection of 16 Theorema theories, consisting in total of roughly 2240 formulas, that may serve as the basis for future theory explorations in Theorema; this, in particular, holds for eight theories exclusively dealing with elementary mathematical concepts, such as sets, numbers, tuples, etc., that are themselves absolutely independent of Gröbner bases, reduction rings and Buchberger's algorithm. Although the mathematical theories we considered for formalization are by no means novel, we nevertheless managed to contribute to them as well, by (drastically) simplifying one proof, generalizing various definitions and results, and, most importantly, correcting a subtle error in the theory of reduction rings. This definitely gives evidence to the claim that mathematics profits from being treated formally in software systems and hence constitutes another motivation for our work in particular and for computer-assisted theory exploration in general. Finally, the thesis also reports on four tools in Theorema we developed in the frame of our studies: a powerful first- and higher-order rewriting mechanism, a set of inference rules for general predicate logic, a versatile proof strategy for interactive proving, and a package of functions for analyzing the logical structure of one or more Theorema theories. Each of these four tools already proved extremely useful during our formal treatment of Gröbner bases theory and will certainly aid future theory explorations in Theorema as well.