User: Guest  Login
Original title:
Formalizing Plane Graph Theory 
Original subtitle:
Towards a Formalized Proof of the Kepler Conjecture 
Translated title:
Formalisierung der Theorie ebener Graphen 
Translated subtitle:
Ein Beitrag zur Formalisierung des Beweises der Keplerschen Vermutung 
Year:
2006 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof. Ph.D.) 
Referee:
Richter-Gebert, Jürgen (Prof. Dr. Dr.) 
Format:
Text 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik; MAT Mathematik 
Keywords:
Formal Verification; Plane graph theory; Kepler conjecture 
Translated keywords:
Formale Verifikation; Theory ebener Graphen; Keplersche Vermutung 
Controlled terms:
Ebener Graph; Formaler Beweis; Automatisches Beweisverfahren 
TUM classification:
DAT 706d; MAT 055d; MAT 052d; MAT 036d 
Abstract:
In 1998, Thomas Hales published a proof of the Kepler Conjecture, which states that the {\em cubic close packing} is the densest possible packing of equally-sized spheres. The proof is by exhaustion on a set of 3050 plane graphs satisfying certain properties, called {\em tame plane graphs}. The enumeration of this set has been generated by a computer program, hence the completeness of this enumeration is essential for the proof. In this thesis, we formalize a theory of plane graphs defined as an...    »
 
Translated abstract:
Im Jahre 1998 veröffentlichte der Mathematiker Thomas Hales einen Beweis der auf Kepler zurückgehenden Vermutung, daß die kubisch dichte Kugelpackung (englisch {\em cubic close packing}) die dichteste Kugelpackung ist. Der Beweis beruht auf einer umfangreichen, durch ein Programm generierten Fallunterscheidung über ca. 3050 Fälle. Dabei wird jeder Fall durch einen ebenen Graphen mit bestimmten Eigenschaften, einem sogenannten {\em zahmen Graphen} repräsentiert. Wesentlich für den Beweis ist die...    »
 
Publication :
Universitätsbibliothek der Technischen Universität München 
Oral examination:
01.02.2006 
File size:
5397278 bytes 
Pages:
188 
Last change:
10.07.2007