The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi.

In http://color.inria.fr, there is a small library on finite graphs 
(http://color.inria.fr/doc/CoLoR.Util.FGraph.FGraph.html) with the 
computation of the transitive closure 
(http://color.inria.fr/doc/CoLoR.Util.FGraph.TransClos.html) based on 
Coq's FMap functor.

Frédéric.


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