Graph Theory in Coq: Minors, Treewidth, and Isomorphisms

Christian Doczkal (1, 2) , Damien Pous (1, 2)

1 PLUME - Preuves et Langages
2 LIP - Laboratoire de l'Informatique du Parallélisme

We present a library for graph theory in Coq/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalise several results from the literature: Menger's theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.

Mots clés: graph theory; minor; treewidth; isomorphisms; Coq; Ssreflect

Domaines: Logique en informatique [cs.LO]

Christian Doczkal, Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-020-09543-2⟩. ⟨hal-02316859v2⟩