Graph theory in Coq: minors, treewidth, and isomorphisms

DOI10.1007/s10817-020-09543-2zbMath1468.68320OpenAlexW3004330900MaRDI QIDQ2209536

Christian Doczkal, Damien Pous

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09543-2

zbMATH Keywords

isomorphismsminorgraph theorytreewidthCoqSsreflect

Mathematics Subject Classification ID

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

Related Items

Hall's theorem for enumerable families of finite sets

Uses Software

• Coq
• Coq/SSReflect
• Flyspeck
• Edmonds-Karp
• Tame Graphs
• Graph Theory
• Hereditarily Finite Sets
• Finite Automata HF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Graph minors. XX: Wagner's conjecture
• Short proof of Menger's theorem
• Conjunctive query containment revisited
• A formal proof of the minor-exclusion property for treewidth-two graphs
• A graph library for Isabelle
• Topology of series-parallel networks
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Formalizing the Edmonds-Karp Algorithm
• Refinements for Free!
• A Formalisation of Finite Automata Using Hereditarily Finite Sets
• The complexity of homomorphism and constraint satisfaction problems seen from the other side
• Flyspeck I: Tame Graphs
• Allegories
• Pragmatic Quotient Types in Coq
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Formal Study of Plane Delaunay Triangulation
• Formalization of the Domination Chain with Weighted Parameters (Short Paper)