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:

- yellow modules: preliminary infrastructure
- orange modules: general purpose graph theory modules
- violet modules: the 2pdom-algebra of graphs and completenes of 2pdom axioms
- red modules: the 2p algebra of graphs and extraction of terms from K4-free graphs
- green modules: hypermaps and Wagner's theorem.

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.

- Graph Theory in Coq - Minors, Treewidth, and Isomorphisms doi:10.1007/s10817-020-09543-2
- Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq doi:10.1145/3372885.3373831
- A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs doi:10.1007/978-3-319-94821-8_11
- Formalization of the Domination Chain with Weighted Parameters (Short Paper) doi:10.4230/LIPIcs.ITP.2019.36

- Christian Doczkal
- Damien Pous
- Daniel Severín (external contributor)