English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The Perfect Graph Theorems are important results in graph theory describingthe 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 PerfectGraph Theorem (SPGT) states that a graph is perfect if and only if it does notcontain an odd hole (or an odd anti-hole) as its induced subgraph. The WeakPerfect Graph Theorem (WPGT) states that a graph is perfect if and only if itscomplement is perfect. In this paper, we present a formal framework for workingwith finite simple graphs. We model finite simple graphs in the Coq ProofAssistant by representing its vertices as a finite set over a countablyinfinite domain. We argue that this approach provides a formal framework inwhich it is convenient to work with different types of graph constructions (orexpansions) 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 theWeak Perfect Graph Theorem.

A Constructive Formalization of the Weak Perfect Graph Theorem