DROPS

Document

Towards a Verified Enumeration of All Tame Plane Graphs

Authors: Tobias Nipkow and Gertrud Bauer

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)

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.

Cite as

Tobias Nipkow and Gertrud Bauer. Towards a Verified Enumeration of All Tame Plane Graphs. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@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/entities/document/10.4230/DagSemProc.05021.21},
  URN =		{urn:nbn:de:0030-drops-4343},
  doi =		{10.4230/DagSemProc.05021.21},
  annote =	{Keywords: Kepler conjecture, certified proofs, flyspeck}
}

Search Results

Documents authored by Bauer, Gertrud

Towards a Verified Enumeration of All Tame Plane Graphs

Abstract

Cite as

Thanks for your feedback!

Could not send message