A lower bound on the size of resolution proofs of the Ramsey theorem

摘要

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