Login
- Original title:
- Flyspeck II: The Basic Linear Programs
- Translated title:
- Flyspeck II: Die elementaren linearen Programme.
- Author:
- Obua, Steven
- Year:
- 2008
- Document type:
- Dissertation
- Faculty/School:
- Fakultät für Informatik
- Advisor:
- Nipkow, Tobias (Prof., Ph.D.)
- Referee:
- Nipkow, Tobias (Prof., Ph.D.); Hales, Thomas C. (Prof.)
- Language:
- en
- Subject group:
- DAT Datenverarbeitung, Informatik; MAT Mathematik
- Keywords:
- Flyspeck, linear programming, HOL, theorem proving
- Translated keywords:
- Flyspeck, lineare Programmierung, HOL, theorem beweisen
- Abstract:
- 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.
- Translated abstract:
- 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.
- WWW:
- https://mediatum.ub.tum.de/?id=645669
- Date of submission:
- 31.01.2008
- Oral examination:
- 21.05.2008
- Pages:
- 100
- Urn (citeable URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20080124-645669-1-1
- Last change:
- 05.01.2009
BibTeX