22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) Some Methods of Problem Solving in Elementary Geometry Wroclaw, Poland July 10-July 14 ISBN: 0-7695-2908-9
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.43
Many elementary problems in geometry arise as part of the proof of the Kepler conjecture on sphere packings. In the original proof, most of these problems were solved by hand. This article investigates the methods that were used in the original proof and describes a number of other methods that might be used to automate the proofs of these problems. A companion article presents the collection of elementary problems in geometry for which automated proofs are sought. This article is a contribution to the Flyspeck project, which aims to give a complete formal proof of the Kepler conjecture.
Citation:
Thomas C. Hales, "Some Methods of Problem Solving in Elementary Geometry," lics, pp.35-40, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb