Graph theory in Coq: minors, treewidth, and isomorphisms

DOI10.1007/s10817-020-09543-2zbMath1468.68320MaRDI 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

isomorphisms; minor; graph theory; treewidth; Coq; Ssreflect

Mathematics Subject Classification ID

05C05: Trees

03B35: Mechanization of proofs and logical operations

05C83: Graph minors

05C40: Connectivity

05C60: Isomorphism problems in graph theory (reconstruction conjecture, etc.) and homomorphisms (subgraph embedding, etc.)

68V20: Formalization of mathematics in connection with theorem provers

Uses Software

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