Introduction to Propositional Proof Complexity

This short seminar series will introduce some fundamental concepts in proof complexity theory, as well as its motivations from complexity theory and connections to logic.

We consider the abstract notion of a propositional proof system and present Cook's theorem, relating the complexity of propositional proofs to fundamental questions in complexity theory, P vs NP and coNP vs NP. Typical systems from undergraduate courses are considered and some basic complexity properties are presented; in particular we expose the complexity gap between systems with cut and cut-free systems.

In order to better understand the complexity of systems with cut, various restrictions on proofs have been proposed. The most well-studied approach is the bounding of depth of formulae occurring in a proof, motivated by circuit complexity theory. We outline textbook results on the complexity of such systems and briefly discuss connections with bounded arithmetic.

Finally we consider a modern approach motivated by the deep inference methodology. We prove the equivalence of these systems to sequent proofs with various restrictions on cut-formulae, and present recent complexity results.

A running example throughout these talks will be propositional encodings of the pigeonhole principle, and how the size of proofs of this encoding varies amongst propositional proof systems.


Preliminaries. Propositional proof systems, Basic complexity theory, Cook's theorem, Other motivating questions.

Frege and Gentzen systems. Robustness of Frege, Dag-like proofs and tree-like proofs, Equivalence of Frege and Gentzen systems, Cost of cut-elimination, Cost of dag-elimination, Polynomial-size proofs of the pigeonhole principle.

Bridging the gap: bounded-depth approach. Bounded-depth Frege systems, Relationship to logic and complexity theory, Special case of resolution, Exponential lower bound on proofs of the pigeonhole principle.

Bridging the gap: analytic deep inference. Analytic deep inference systems, Formulation as restrictions on cut-formulae, Relative complexity results, Quasipolynomial-size proofs of the pigeonhole principle.

Useful References

Buss, Samuel R. "Propositional proof complexity an introduction." In Computational Logic, pp. 127-178. Springer Berlin Heidelberg, 1999.

Cook, Stephen A. "The complexity of theorem-proving procedures." In Proceedings of the third annual ACM symposium on Theory of computing, pp. 151-158. ACM, 1971.

Buss, Samuel R. "Polynomial size proofs of the propositional pigeonhole principle." Journal of Symbolic Logic (1987): 916-927.

Paris, Jeff, and A.J. Wilkie, "Delta-0 sets and induction." Proceedings of the Jadwisin Logic Conference, pp.237-248. Leeds University Press, 1981.

Pitassi, Toniann, Paul Beame, and Russell Impagliazzo. "Exponential lower bounds for the pigeonhole principle." Computational complexity 3, no. 2 (1993): 97-140.

Krajicek, Jan. Bounded arithmetic, propositional logic and complexity theory. Cambridge University Press, 1995.

Atserias, Albert, Nicola Galesi, and Ricard Gavalda. "Monotone proofs of the pigeon hole principle." Mathematical Logic Quarterly 47, no. 4 (2001): 461-474.

Bruscoli, Paola, and Alessio Guglielmi. "On the proof complexity of deep inference." ACM Transactions on Computational Logic (TOCL) 10, no. 2 (2009): 14.

Das, Anupam. "Complexity of deep inference via atomic flows." In How the World Computes, pp. 139-150. Springer Berlin Heidelberg, 2012.