Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twenty-Second Annual IEEE Symposium on

Logic in Computer Science (LICS 2007)

Invited Paper: Some Methods of Problem Solving in Elementary Geometry (at LICS 2007)

Authors: Thomas C. Hales

Abstract

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.

BibTeX

  @InProceedings{Hales-SomeMethodsofProble,
    author = 	 {Thomas C. Hales},
    title = 	 {Some Methods of Problem Solving in Elementary Geometry},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {35--40},
    location =   {Wroclaw, Poland}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski