Benutzer: Gast  Login
Wenn Sie Schwierigkeiten haben, das Dokument zu öffnen, versuchen Sie auch bitte diesen Link
Originaltitel:
Big Math in Interactive Theorem Provers: Scaling the Isabelle Archive of Formal Proofs
Übersetzter Titel:
Großangelegte Mathematik in Interaktiven Theorembeweisern: Skalierung des Isabelle Archive of Formal Proofs
Autor:
Huch, Fabian
Jahr:
2026
Dokumenttyp:
Dissertation
Fakultät/School:
TUM School of Computation, Information and Technology
Institution:
Informatik 21 - Lehrstuhl für Logik und Verifikation (N.N.)
Betreuer:
Nipkow, Tobias (Prof., Ph.D.)
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Kohlhase, Michael (Prof. Dr.)
Sprache:
en
Fachgebiet:
DAT Datenverarbeitung, Informatik
TU-Systematik:
DAT 706; DAT 540
Kurzfassung:
In this thesis, I approach problems arising with large-scale formalization of mathematics in interactive theorem provers, on the example of the Isabelle system and its Archive of Formal Proofs. To that end, I investigate properties of formal entity dependency graphs, analyze the impact of anti-patterns on maintenance effort and quality, and benchmark proof checking times. Based on that, I develop a distributed build system and tools to address maintenance problems via similarity search.
Übersetzte Kurzfassung:
In dieser Arbeit behandle ich am Beispiel von Isabelle und dem Archive of Formal Proofs einige Probleme, die bei großangelegter Formalisierung von Mathematik in interaktiven Theorembeweisern auftreten. Dazu untersuche ich Eigenschaften von Abhängigkeitsgraphen formaler Entitäten, analysiere Auswirkungen von anti-Patterns auf den Wartungsaufwand, und analysiere Laufzeit der Beweisprüfung. Darauf basierend entwickle ich ein verteiltes Build-system sowie Werkzeuge, um Wartungsprobleme anzugehen.
WWW:
https://mediatum.ub.tum.de/?id=1796789
Eingereicht am:
19.09.2025
Mündliche Prüfung:
30.03.2026
Dateigröße:
7060232 bytes
Seiten:
162
Urn (Zitierfähige URL):
https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20260330-1796789-0-4
Veröffentlicht am:
09.04.2026
 BibTeX