Benutzer: Gast  Login
Originaltitel:
Flyspeck II: The Basic Linear Programs 
Übersetzter Titel:
Flyspeck II: Die elementaren linearen Programme. 
Jahr:
2008 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Hales, Thomas C. (Prof.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik; MAT Mathematik 
Stichworte:
Flyspeck, linear programming, HOL, theorem proving 
Übersetzte Stichworte:
Flyspeck, lineare Programmierung, HOL, theorem beweisen 
Kurzfassung:
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. 
Mündliche Prüfung:
21.05.2008 
Seiten:
100 
Letzte Änderung:
05.01.2009