The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Hello Christian,

this library:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fingraph.v

is about the elementary theory of finite graphs (with decidable node equality
and edge relation). It depends on this other library, about paths:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/path.v

which you might also find useful.

Both derive from a file used for representing the graphs in the Four Colour
Theorem formal proof.

But I am not aware of any Coq formal library related to minors or tree-width.

Best,

assia

Le 13/06/2017 à 14:59, Christian Doczkal a écrit :
> Hello,
> 
> Does anyone know if there are any Coq developments out there that
> formalize (some) standard notions from graph theory.
> 
> I'm particularly interested in finite graphs (with decidable node
> equality and edge relations), minors, and tree decompositions. Basic
> results I would be looking for include the fact that the tree-width of a
> graphs minor is no greater than the tree-width of the original graph or
> that every clique contained in a graph must be contained in some bag of
> every tree decomposition.
> 
> Best,
> Christian
>