Start learning proof complexity

• Have you checked the references in the Wikipedia article proof complexity? Steve and Phuong's book is relatively easy to read. Oct 9, 2013 at 17:06
• I enjoyed the presentation given by Olaf Beyersdorff in Helsinki this summer. Check out his slides here.
– Juho
Oct 9, 2013 at 17:10

It depends on what kind of a "beginner" level you wish to have. I don't think there is a real good undergraduate level text on proof complexity (this is probably true for most specialized sub-areas in complexity). But for a beginner (graduate level) sources, I would recommend, something like understanding well the basic exponential size lower bound on resolution refutations of the pigeonhole principle (via random restrictions, width-size tradeoff and feasible interpolation), and to expand from that point further. This could be achieved (approximately) as follows:

1. Stasys Jukna, Extremal Combinatorics With Applications in Computer Science, 2001, Springer-Verlag, Section 4.8.

2. Eli Ben-sasson and Avi Wigderson, Short Proofs are Narrow - Resolution made Simple (2000), JACM.

3. P. Beame and T. Pitassi, Propositional proof complexity: Past, present, and future, Current trends in theoretical computer science: Entering the 21st century (G. Paul, G. Rozenberg, and A. Salomaa, editors), World Scientific Publishing, 2001, pp. 42--70.

4. Pavel Pudlák, Lower bounds for resolution and cutting planes proofs and monotone computations, The Journal of Symbolic Logic, vol. 62 (1997), no. 3, pp. 981-998.

You can also consult the more self contained and lengthy text:

• Peter Clote and Evangelos Kranakis, Boolean Functions and Computation Models (Chapter 5)

For the more logical side of proof complexity, as Kaveh suggested, you can start reading the first chapters of:

• Stephen Cook and Phuong Nguyen, Logical Foundations of Proof Complexity (Perspectives in Logic, Cambridge Press, 2010).
• Thank you very much! I will dig in to these and see how they turn out Oct 10, 2013 at 11:10

For the more algebraic side of proof complexity I recommend starting with Pitassi's 1996 survey paper:

• T. Pitassi. Algebraic propositional proof systems, in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Volume 31, Descriptive Complexity and Finite Models, Immerman and Kolaitis (Eds.), pp. 215-244, 1996.

For a quick overview you might also consult Chapter 5 of the Clote--Kranakis book already mentioned by Iddo, which has a section on algebraic proof systems.

The first research paper I'd recommend reading (both because it's seminal and because it's a pleasant read) is the paper in which the Groebner or Polynomial Calculus proof system was introduced:

I find these introductory lecture notes easy to read: Paul Beame's IAS Lectures

• The notes from Paul Beame's IAS lectures are very nice and give a good overview of the area. One thing to be aware of, though, is that there are some problems with some statements of the "if pigs can fly" type theorems. I tried to give corrected versions in (the mini-survey in) Chapter 4 of my PhD thesis: Jakob Nordström. Short Proofs May Be Spacious: Understanding Space in Resolution. PhD thesis, Royal Institute of Technology, Stockholm, Sweden, May 2008 (www.csc.kth.se/~jakobn/research/PhDthesis.pdf). Oct 28, 2013 at 21:48

The most recent and up-to-date general-purpose proof complexity survey is probably that of Nathan Segerlind:

Nathan Segerlind: The Complexity of Propositional Proofs. Bulletin of Symbolic Logic 13(4): 417-481, 2007 (http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps).

And now, warnings for two shameless self plugs…

An even more recent survey, but more narrowly focused on questions regarding proof size, proof space, and size-space trade-offs, is:

Jakob Nordström. Pebble Games, Proof Complexity, and Time-Space Trade-offs. Logical Methods in Computer Science, volume 9, issue 3, article 15, September 2013 (http://www.lmcs-online.org/ojs/viewarticle.php?id=674).

There are also some lecture notes from a somewhat recent course I gave on the "low-end spectrum" of proof complexity (i.e., comparatively weak proof systems such as resolution, polynomial calculus, and cutting planes) and connections to SAT solving. These notes can be found at http://www.csc.kth.se/~jakobn/teaching/proofcplx11/#scribe-notes (some are still in progress but the ones that are available should be in good shape).