We prove an exponential lower bound on the lengths of resolution proofs of propositions expressing the finite Ramsey theorem for pairs.

more >>>

Ramsey theory assures us that in any graph there is a clique or independent set of a certain size, roughly logarithmic in the graph size. But how difficult is it to find the clique or independent set? If the graph is given explicitly, then it is possible to do so ... more >>>