Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Nipkow, Tobias; Bauer, Gertrud License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-4343


Towards a Verified Enumeration of All Tame Plane Graphs



In his proof of the Kepler conjecture, Thomas Hales introduced the notion of tame graphs and provided a Java program for enumerating all tame plane graphs. We have translated his Java program into an executable function in HOL ("the generator"), have formalized the notions of tameness and planarity in HOL, and have partially proved that the generator returns all tame plane graphs. Running the generator in ML has shows that the list of plane tame graphs ("the archive") that Thomas Hales also provides is complete. Once we have finished the completeness proof for the generator. In addition we checked the redundancy of the archive by formalising an executable notion of isomorphism between plane graphs, and checking if the archive contains only graphs produced by the generator. It turned out that 2257 of the 5128 graphs in the archive are either not tame or isomorphic to another graph in the archive.

BibTeX - Entry

  author =	{Tobias Nipkow and Gertrud Bauer},
  title =	{Towards a Verified Enumeration of All Tame Plane Graphs},
  booktitle =	{Mathematics, Algorithms, Proofs},
  year =	{2006},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran{\c{c}}oise Roy},
  number =	{05021},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{},
  annote =	{Keywords: Kepler conjecture, certified proofs, flyspeck}

Keywords: Kepler conjecture, certified proofs, flyspeck
Seminar: 05021 - Mathematics, Algorithms, Proofs
Issue date: 2006
Date of publication: 17.01.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI