This thesis is the second major contribution to the Flyspeck project which
has as its goal the complete machine-verified formalization of the proof of the Kepler conjecture that Thomas Hales has given in 1998.
We specify, generate and bound what Hales loosely calls the basic linear programs.
We do this within the interactive proof assistant Isabelle.
There are two major aspects of this work: Logical reasoning and trusted computing. Of course trusted computing can be considered as a special case of logical reasoning but
requirements regarding the speed of computing demand a special treatment. Our solution to this problem is the HOL Computing Library. A substantial part of this work is dedicated to the design
and implementation of this library. We then apply the library to show that 92.5% of all tame graphs give raise to basic linear programs which are inconsistent.
Übersetzte Kurzfassung:
Diese Arbeit ist der zweite größere Beitrag zum Flyspeck-Projekt, dessen Ziel die vollständige maschinelle Verifikation des Beweises der Keplerschen Vermutung ist, den Thomas Hales 1998 gegeben hat.
Wir spezifizieren, generieren, und berechnen Schranken für die von Hales sogenannten elementaren linearen Programme, und zwar innerhalb des interaktiven Beweisassistenten Isabelle.
Zwei Aspekte sind dabei prägend: Logisches Schließen und verlässliches Rechnen. Natürlich kann verlässliches Rechnen als Spezialfall von logischem Schließen angesehen werden aber Anforderungen an die
Rechengeschwindigkeit verlangen nach einer gesonderten Lösung. Als solche stellen wir ein Programmpaket für verlässliches Rechnen vor. Ein beträchtlicher Teil unserer Arbeit ist dem Design und der Implementierung dieses Programmpakets gewidmet. Mit seiner Hilfe beweisen wir, dass 92,5% aller zahmen Graphen elementare lineare Programme induzieren, die inconsistent sind.
Login
BibTeX