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

Abstract : 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.
Type de document :
Communication dans un congrès
Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. 〈10.1007/978-3-319-94821-8_11〉
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01703922
Contributeur : Damien Pous <>
Soumis le : mercredi 12 septembre 2018 - 10:32:17
Dernière modification le : jeudi 13 septembre 2018 - 01:15:52

Fichier

tw2k4f.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

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〉

Partager

Métriques

Consultations de la notice

53

Téléchargements de fichiers

8