The complexity of proving that a graph is Ramsey

Massimo Lauria, Pavel Pudlák, Vojtěch Rödl +1

We say that a graph with $n$ vertices is $c$-Ramsey if it does not contain either a clique or an independent set of size $c\log n$. We define a CNF formula which expresses this pr…