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/

Zendy Plus

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

Zendy Tools

Zendy Open

Interaction between clique number $\omega(G) $ and chromatic number $\chi(G)$ of a graph is a well studied topic in graph theory. Perfect Graph Theoremsare probably the most important results in this direction. 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 andonly if it does not contain an odd hole (or an odd anti-hole) as its inducedsubgraph. The Weak Perfect Graph Theorem (WPGT) states that a graph is perfectif and only if its complement is perfect. In this paper, we present a formalframework for verifying these results. We model finite simple graphs in theconstructive type theory of Coq Proof Assistant without adding any axiom to it.Finally, we use this framework to present a constructive proof of theLov\'{a}sz Replication Lemma, which is the central idea in the proof of WeakPerfect Graph Theorem.

Towards a constructive formalization of Perfect Graph Theorems