-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathmeta.yml
161 lines (135 loc) · 5.41 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
---
fullname: Graph Theory
shortname: graph-theory
organization: coq-community
community: true
action: true
coqdoc: false
doi: 10.1007/s10817-020-09543-2
chat:
url: https://coq.zulipchat.com/#narrow/stream/284683-GraphTheory
shield: Zulip
synopsis: >-
Graph theory definitions and results in Coq and MathComp
description: |-
A library of formalized graph theory results, including various
standard results from the literature (e.g., Menger's Theorem, Hall's
Marriage Theorem, the excluded minor characterization of
treewidth-two graphs, and Wagner's Theorem) as well as some more
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).
publications:
- pub_url: https://hal.inria.fr/hal-03142192
pub_title: A Variant of Wagner's Theorem Based on Combinatorial Hypermaps
pub_doi: 10.4230/LIPIcs.ITP.2021.17
- pub_url: https://hal.archives-ouvertes.fr/hal-02316859
pub_title: Graph Theory in Coq - Minors, Treewidth, and Isomorphisms
pub_doi: 10.1007/s10817-020-09543-2
- pub_url: https://hal.archives-ouvertes.fr/hal-02333553
pub_title: Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
pub_doi: 10.1145/3372885.3373831
- pub_url: https://hal.archives-ouvertes.fr/hal-01703922
pub_title: A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
pub_doi: 10.1007/978-3-319-94821-8_11
- pub_url: https://drops.dagstuhl.de/opus/volltexte/2019/11091/
pub_title: Formalization of the Domination Chain with Weighted Parameters (Short Paper)
pub_doi: 10.4230/LIPIcs.ITP.2019.36
authors:
- name: Christian Doczkal
initial: true
- name: Damien Pous
initial: true
after_authors: |2
- Daniel Severín (external contributor)
maintainers:
- name: Christian Doczkal
nickname: chdoc
- name: Damien Pous
nickname: damien-pous
opam-file-maintainer: christian.doczkal@mpi-sp.org
opam-file-version: dev
license:
fullname: CeCILL-B
identifier: CECILL-B
supported_coq_versions:
text: 8.18 or later
opam: '{>= "8.18"}'
tested_coq_opam_versions:
- version: 'rocq-prover-dev'
repo: 'mathcomp/mathcomp-dev'
- version: '2.2.0-coq-8.20'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
ci_cron_schedule: '25 5 * * 5'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.1.0"}'
description: MathComp's [SSReflect library](https://math-comp.github.io), version 2.1.0 or later
- opam:
name: coq-mathcomp-algebra
description: MathComp's [Algebra library](https://math-comp.github.io)
- opam:
name: coq-mathcomp-finmap
description: MathComp's [finmap library](https://github.com/math-comp/finmap)
- opam:
name: coq-mathcomp-algebra-tactics
description: MathComp's [Algebra tactics](https://github.com/math-comp/algebra-tactics)
- opam:
name: coq-hierarchy-builder
version: '{>= "1.5.0"}'
description: '[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder), version 1.5.0 or later'
- opam:
name: coq-fourcolor
description: Gonthier's [formal proof](https://github.com/coq-community/fourcolor) of the Four-Color Theorem (optional dependency)
namespace: GraphTheory
keywords:
- name: graph theory
- name: minors
- name: treewidth
- name: algebra
categories:
- name: Computer Science/Graph Theory
build: |-
## Building and installation instructions
To manually build and install the whole project, including Wagner's theorem which requires
the Coq proof of the Four-Color Theorem, do:
``` shell
git clone https://github.com/coq-community/graph-theory.git
cd graph-theory
make # or make -j <number-of-cores-on-your-machine>
make install
```
However, the easiest way to install released versions of Graph Theory
libraries selectively is via [opam](https://opam.ocaml.org/doc/Install.html):
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-graph-theory # core library
opam install coq-graph-theory-planar # planarity results depending on coq-fourcolor
```
documentation: |-
## Documentation
This project contains:
- a general purpose Coq library about graph theory:
- directed graphs, simple graphs, multigraphs
- paths, trees, forests, isomorphism, connected components, etc.
- minors and tree decompositions
- Menger's theorem and some of its corollaries (Hall's marriage theorem and König's theorem)
- the excluded-minor characterisation of treewidth at most two graphs (as those excluding K4 as a minor)
- soundness and completeness of an axiomatization of isomorphism of two-pointed treewidth-two (`2p`) multigraphs:
- isomorphisms up to label-equivalence and edge-flipping for multigraphs
- 2p graphs form a 2p algebra and thus also a 2pdom algebra
- every K4-free graph can be represented by a 2p-term
- 2pdom axioms are complete w.r.t. graph isomorphism for connected 2p graphs.
- a proof of Wagner's theorem (planarity of K5 and K3,3 graphs) based on combinatorial hypermaps
- two proofs of the weak perfect graph theorem (WPGT):
- one proof based on Lovasz's replication lemma
- one proof based on a matrix rank argument
Additional information on the contents of individual files is available at the [project website](https://perso.ens-lyon.fr/damien.pous/covece/graphs/).
---