Lorenzo Carlucci, Nicola Galesi, Massimo Lauria

We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. In particular we study the proof complexity of Paris-Harrington's Large Ramsey Theorem. We prove a conditional lower bound in Resolution and a quasipolynomial upper bound in bounded-depth Frege.

more >>>Massimo Lauria

Ramsey Theorem is a cornerstone of combinatorics and logic. In its

simplest formulation it says that there is a function $r$ such that

any simple graph with $r(k,s)$ vertices contains either a clique of

size $k$ or an independent set of size $s$. We study the complexity

of proving upper ...
more >>>

Massimo Lauria, Pavel Pudlak, Vojtech Rodl, Neil Thapen

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 property for a graph $G$. We show a superpolynomial lower bound on the length of ... more >>>