A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs

Christian Doczkal (1, 2) , Guillaume Combette (1, 2) , Damien Pous (1, 2)

1 PLUME - Preuves et Langages
2 LIP - Laboratoire de l'Informatique du Parallélisme

We give a formal and constructive proof in Coq/Ssreflect of the known result that the graphs of treewidth two are exactly those that do not admit K4 as a minor. This result is a milestone towards a formal proof of the recent result that isomorphism of treewidth-two graphs can be finitely axiomatized. The proof is based on a function extracting terms from K4-free graphs in such a way that the interpretation of an extracted term yields a treewidth-two graph isomorphic to the original graph.

Mots clés: graph theory; Ssreflect; Coq; graph minor theorem

Domaines: Logique en informatique [cs.LO]; Mathématique discrète [cs.DM]

Christian Doczkal, Guillaume Combette, Damien Pous. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. ⟨10.1007/978-3-319-94821-8_11⟩. ⟨hal-01703922v2⟩