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

## Authors: Christian Doczkal, Guillaume Combette and Damien Pous

## Paper Information

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

Authors: | Christian Doczkal, Guillaume Combette and Damien Pous |

Proceedings: | ITP Papers |

Editors: | Jeremy Avigad and Assia Mahboubi |

Keywords: | graph theory, graph minor theorem, formal proofs, Coq, Ssreflect |

Abstract: | 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. |

Pages: | 18 |

Talk: | Jul 12 09:00 (Session 70C) |

Paper: |