A Variant of Wagner's Theorem Based on Combinatorial Hypermaps - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

Résumé

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 K5 nor K3,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 K5 nor K3,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 K5 and K3,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.
Fichier principal
Vignette du fichier
LIPIcs-ITP-2021-17.pdf (701.38 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03142192 , version 1 (15-02-2021)
hal-03142192 , version 2 (02-02-2022)

Licence

Paternité

Identifiants

  • HAL Id : hal-03142192 , version 2

Citer

Christian Doczkal. A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome, Italy. pp.17:1--17:17. ⟨hal-03142192v2⟩
182 Consultations
165 Téléchargements

Partager

Gmail Facebook X LinkedIn More