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: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13912/
Doczkal, Christian
A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps
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}
}
