A formal proof of the minor-exclusion property for treewidth-two graphs

DOI10.1007/978-3-319-94821-8_11zbMath1468.68319OpenAlexW2810735788MaRDI QIDQ1791156

Guillaume Combette, Damien Pous, Christian Doczkal

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_11

zbMATH Keywords

graph theoryCoqSsreflectgraph minor theorem

Mathematics Subject Classification ID

Trees (05C05) Mechanization of proofs and logical operations (03B35) Graph minors (05C83) Isomorphism problems in graph theory (reconstruction conjecture, etc.) and homomorphisms (subgraph embedding, etc.) (05C60) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Hall's theorem for enumerable families of finite sets ⋮ Unnamed Item ⋮ Graph theory in Coq: minors, treewidth, and isomorphisms ⋮ Formalization of the Domination Chain with Weighted Parameters (Short Paper)

Uses Software

• Coq
• Isabelle/HOL
• Coq/SSReflect
• Tame Graphs

This page was built for publication: A formal proof of the minor-exclusion property for treewidth-two graphs