The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi Frédéric,

Thanks for the pointer. I had already looked at CoLoR and come to the
conclusion that for my use case it does not offer much that MathComp
doesn't offer, which I'm using anyways.

MathComp includes relations/paths over finite types with transitive
closure and several other useful lemmas. However, as far as I know,
nothing on minors and tree decompositions.

Best,
Christian



On 14/06/17 18:04, Frédéric Blanqui wrote:
> 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
>