Document

# A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps

## File

LIPIcs.ITP.2021.17.pdf
• Filesize: 0.68 MB
• 17 pages

## Cite As

Christian Doczkal. A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.17

## 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.

## Subject Classification

##### ACM Subject Classification
• Mathematics of computing → Graphs and surfaces
• Theory of computation → Logic and verification
• Coq
• MathComp
• Graph-Theory
• Hypermaps
• Planarity

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0
PDF Downloads

## References

1. Adrian Bondy and U.S.R. Murty. Graph Theory, volume 244 of Graduate Texts in Mathematics. Springer-Verlag London, 2008.
2. Ching-Tsun Chou. A formal theory of undirected graphs in higher-order logic. In TPHOL, volume 859 of LNCS, pages 144-157. Springer, 1994. URL: https://doi.org/10.1007/3-540-58450-1_40.
3. Ching-Tsun Chou. Mechanical verification of distributed algorithms in higher-order logic*. The Computer Journal, 38(2):152-161, January 1995. URL: https://doi.org/10.1093/comjnl/38.2.152.
4. Robert Cori. Un code pour les graphes planaires et ses applications. PhD thesis, Univ. Paris VII, 1973.
5. Reinhard Diestel. Graph Theory (2nd edition). Graduate Texts in Mathematics. Springer, 2000.
6. Christian Doczkal, Guillaume Combette, and Damien Pous. A formal proof of the minor-exclusion property for treewidth-two graphs. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving (ITP 2018), volume 10895 of LNCS, pages 178-195. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_11.
7. Christian Doczkal and Damien Pous. Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. In Proc. of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20), January 20-21, 2020, New Orleans, LA, USA, 2020. URL: https://doi.org/10.1145/3372885.3373831.
8. Christian Doczkal and Damien Pous. Graph theory in Coq: Minors, treewidth, and isomorphisms. J. Autom. Reason., 64(5):795-825, 2020. URL: https://doi.org/10.1007/s10817-020-09543-2.
9. Georges Gonthier. A computer-checked proof of the four colour theorem, 2005. URL: https://www.cl.cam.ac.uk/~lp15/Pages/4colproof.pdf.
10. Georges Gonthier. Formal proof - the four-color theorem. Notices Amer. Math. Soc., 55(11):1382-1393, 2008. URL: http://www.ams.org/notices/200811/tx081101382p.pdf.
11. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean Mclaughlin, and Tat Thang Nguyen. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, 2017. URL: https://doi.org/10.1017/fmp.2017.1.
12. Yatsuka Nakamura and Piotr Rudnicki. Euler circuits and paths. Formalized Mathematics, 6(3):417–425, 1997.
13. Lars Noschinski. Formalizing Graph Theory and Planarity Certificates. PhD thesis, Technische Universität München, 2016.
14. Daniel E. Severín. Formalization of the domination chain with weighted parameters (short paper). In John Harrison, John O'Leary, and Andrew Tolmach, editors, Interactive Theorem Provin (ITP 2019), volume 141 of LIPIcs, pages 36:1-36:7. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.36.
15. Abhishek Kr Singh and Raja Natarajan. A constructive formalization of the weak perfect graph theorem. In Proc. of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20), January 20-21, 2020, New Orleans, LA, USA, 2020. URL: https://doi.org/10.1145/3372885.3373819.
16. Saul Stahl. A combinatorial analog of the Jordan curve theorem. J. Comb. Theory, Ser. B, 35(1):28-38, 1983. URL: https://doi.org/10.1016/0095-8956(83)90078-3.
17. William T. Tutte. Duality and trinity. In Colloquium Mathematical Society Janos Bolyai 10, pages 1459-1472, 1975.
18. David W. Walkup. How many ways can a permutation be factored into two n-cycles? Discret. Math., 28(3):315-319, 1979. URL: https://doi.org/10.1016/0012-365X(79)90138-9.