License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05021.21
URN: urn:nbn:de:0030-drops-4343
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/434/
Go to the corresponding Portal

Nipkow, Tobias ; Bauer, Gertrud

Towards a Verified Enumeration of All Tame Plane Graphs

pdf-format:
05021.NipkowTobias.Paper.434.pdf (0.3 MB)

Abstract

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

@InProceedings{nipkow_et_al:DagSemProc.05021.21,
  author =	{Nipkow, Tobias and Bauer, Gertrud},
  title =	{{Towards a Verified Enumeration of All Tame Plane Graphs}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/434},
  URN =		{urn:nbn:de:0030-drops-4343},
  doi =		{10.4230/DagSemProc.05021.21},
  annote =	{Keywords: Kepler conjecture, certified proofs, flyspeck}
}

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

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