View the project on GitHub
Welcome to the Graph Theory GitHub website! This project is part of coq-community.
This is a library of formalized graph theory results, including various standard results from the literature (e.g., Menger’s Theorem, Hall’s Marriage Theorem, and the excluded minor characterization of treewidth-two graphs). The library also includes a proof of Wagner's theorem based on the combinatorial hypermaps developed for the proof of the four-color theorem and machine-checked proofs of recent results arising from the study of relation algebra within the ERC CoVeCe project (e.g., soundness and completeness of an axiomatization of graph isomorphism).
This is an open source project, licensed under the CeCILL-B.
Large parts of this library have been develped as part of the ERC CoVeCe project. See also the CoVeCe Graph-Theory project page.
The current stable release of Graph Theory can be downloaded from GitHub or installed via OPAM (package coq-graph-theory).
The library consists of several interconnected parts:
The coqdoc documentation of the library can be accessed via the links below or by clicking on one of the nodes in the graph to go directly to the latest documentation for that module.
The library is the subject of serveral publications, which are listed below.