Write a Blog >>
Tue 21 Jan 2020 15:56 - 16:18 at Maurepas - Formalized mathematics 1 Chair(s): Robert Y. Lewis

The Perfect Graph Theorems are important results in graph theory describing the relationship between clique number $\omega(G) $ and chromatic number $\chi(G) $ of a graph $G$. A graph $G$ is called \emph{perfect} if $\chi(H)=\omega(H)$ for every induced subgraph $H$ of $G$. The Strong Perfect Graph Theorem (SPGT) states that a graph is perfect if and only if it does not contain an odd hole (or an odd anti-hole) as its induced subgraph. The Weak Perfect Graph Theorem (WPGT) states that a graph is perfect if and only if its complement is perfect. In this paper, we present a formal framework for working with finite simple graphs. We model finite simple graphs in the Coq Proof Assistant by representing its vertices as a finite set over a countably infinite domain. We argue that this approach provides a formal framework in which it is convenient to work with different types of graph constructions (or expansions) involved in the proof of the Lov'{a}sz Replication Lemma (LRL), which is also the key result used in the proof of Weak Perfect Graph Theorem. Finally, we use this setting to develop a constructive formalization of the Weak Perfect Graph Theorem.

Slides (cpp_ppt.pdf)401KiB

Tue 21 Jan (GMT-06:00) Saskatchewan, Central America change

15:35 - 16:40: CPP 2020 - Formalized mathematics 1 at Maurepas
Chair(s): Robert Y. LewisVrije Universiteit Amsterdam
CPP-2020-papers15:35 - 15:56
Patrick MassotUniversité Paris Sud, Kevin BuzzardImperial College London, Johan CommelinUniversität Freiburg
DOI Pre-print Media Attached File Attached
CPP-2020-papers15:56 - 16:18
Abhishek Kr SinghTata Institute of Fundamental Research Mumbai, Raja NatarajanTata Institute of Fundamental Research Mumbai
DOI Pre-print Media Attached File Attached
CPP-2020-papers16:18 - 16:40
Christian DoczkalUniversité Côte d'Azur, Damien PousCNRS, ENS Lyon
DOI Pre-print Media Attached