The Computer Science Colloquium

Stephen Cook
(University of Toronto)

"Computational Complexity and Proofs of Combinatorial Principles"

The fundamental problem of complexity theory is P =? NP: Can every nondeterministic polynomial time algorithm be made deterministic? An important related problem is NP =? coNP, which holds iff there exists a propositional proof system in which all tautologies have polynomial size proofs. The prevailing view is that the answer to both questions is no. But it is remarkably hard to prove superpolynomial lower bounds on proof length even for common proof systems. We will explain the significance of proving lower bounds and describe what progress has been made here. The strength of a proof system is related to the complexity of the concepts expressible by a line in the proof. This motivates a study of the complexity of concepts required to prove combinatorial principles.

The Colloquium is supported by generous contributions from the Bloomberg, Information Builders, Inc. and Netlogic, Inc.