License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.17
URN: urn:nbn:de:0030-drops-139123
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13912/
Go to the corresponding LIPIcs Volume Portal


Doczkal, Christian

A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps

pdf-format:
LIPIcs-ITP-2021-17.pdf (0.7 MB)


Abstract

Wagner’s theorem states that a graph is planar (i.e., it can be embedded in the real plane without crossing edges) iff it contains neither 𝖪_5 nor 𝖪_{3,3} as a minor. We provide a combinatorial representation of embeddings in the plane that abstracts from topological properties of plane embeddings (e.g., angles or distances), representing only the combinatorial properties (e.g., arities of faces or the clockwise order of the outgoing edges of a vertex). The representation employs combinatorial hypermaps as used by Gonthier in the proof of the four-color theorem. We then give a formal proof that for every simple graph containing neither 𝖪_5 nor 𝖪_{3,3} as a minor, there exists such a combinatorial plane embedding. Together with the formal proof of the four-color theorem, we obtain a formal proof that all graphs without 𝖪_5 and 𝖪_{3,3} minors are four-colorable. The development is carried out in Coq, building on the mathematical components library, the formal proof of the four-color theorem, and a general-purpose graph library developed previously.

BibTeX - Entry

@InProceedings{doczkal:LIPIcs.ITP.2021.17,
  author =	{Doczkal, Christian},
  title =	{{A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13912},
  URN =		{urn:nbn:de:0030-drops-139123},
  doi =		{10.4230/LIPIcs.ITP.2021.17},
  annote =	{Keywords: Coq, MathComp, Graph-Theory, Hypermaps, Planarity}
}

Keywords: Coq, MathComp, Graph-Theory, Hypermaps, Planarity
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: All proofs in this paper have been formalized using the Coq interactive theorem prover and are included in version 0.9 of the coq-community/graph-theory library:
Software (Code Repository): https://github.com/coq-community/graph-theory archived at: https://archive.softwareheritage.org/swh:1:dir:81966a945703d0e2a85fe34e920f4fe9a46b6e03


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