<p>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:</p>

<ol>
<li><p>Stasys Jukna, Extremal Combinatorics With Applications in Computer Science, 2001, Springer-Verlag, Section 4.8.</p></li>
<li><p>Eli Ben-sasson and Avi Wigderson, Short Proofs are Narrow - Resolution made Simple (2000), JACM.</p></li>
<li><p>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.</p></li>
<li><p>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. </p></li>
</ol>

<p>You can also consult the more self contained and lengthy text:</p>

<ul>
<li>Peter Clote and Evangelos Kranakis, Boolean Functions and Computation Models (Chapter 5)</li>
</ul>

<p>For the more <em>logical</em> side of proof complexity, as Kaveh suggested, you can start reading the first chapters of:</p>

<ul>
<li>Stephen Cook and Phuong Nguyen, Logical Foundations of Proof Complexity (Perspectives in Logic, Cambridge Press, 2010).</li>
</ul>

CC BY-SA 3.0
2013-10-10T11:10:53.337Z
Thank you very much! I will dig in to these and see how they turn out
Yugioh Mishima
CC BY-SA 3.0
2013-10-10T10:54:54.823Z
2013-11-11T18:51:35.953Z
2013-11-11T18:51:35.953Z
Iddo Tzameret
<p>I find these introductory lecture notes easy to read: <a href="http://www.cs.cornell.edu/~sabhar/publications/iaspcmi-proofcomplexity00.pdf">Paul Beame's IAS Lectures</a></p>

CC BY-SA 3.0
2013-10-28T21:48:45.150Z
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](http://www.csc.kth.se/~jakobn/research/PhDthesis.pdf)).
Jakob Nordstrom
CC BY-SA 3.0
2013-10-11T09:33:01.397Z
2013-10-11T09:33:01.397Z
Dai Le
<p>For the more algebraic side of proof complexity I recommend starting with Pitassi's 1996 survey paper:</p>

<ul>
<li>T. Pitassi. <a href="http://www.cs.toronto.edu/~toni/Papers/pitassi-algebraic.ps">Algebraic propositional proof systems</a>, 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.</li>
</ul>

<p>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.</p>

<p>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:</p>

<ul>
<li>Clegg, Matthew; Edmonds, Jeffery; Impagliazzo, Russell. <a href="http://dx.doi.org/10.1145/237814.237860">Using the Groebner basis algorithm to find proofs of unsatisfiability</a> STOC 1996, 174-183. (Also available from author's webpages without paywall.)</li>
</ul>

CC BY-SA 3.0
2013-10-10T14:10:07.753Z
2013-10-10T14:10:07.753Z
Joshua Grochow
<p>The most recent and up-to-date general-purpose proof complexity survey is probably that of Nathan Segerlind:</p>

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

<p>And now, warnings for two shameless self plugs&hellip;</p>

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

<p><em>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 (<a href="http://www.lmcs-online.org/ojs/viewarticle.php?id=674">http://www.lmcs-online.org/ojs/viewarticle.php?id=674</a>).</em></p>

<p>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 <a href="http://www.csc.kth.se/~jakobn/teaching/proofcplx11/#scribe-notes">http://www.csc.kth.se/~jakobn/teaching/proofcplx11/#scribe-notes</a> (some are still in progress but the ones that are available should be in good shape).</p>

CC BY-SA 3.0
2013-10-28T22:30:22.803Z
2013-10-28T22:30:22.803Z
Jakob Nordstrom
<p>I recently started to read a lot about proof complexity and have been really enjoying what I have been reading. I would really like to learn more about this, but I am having difficulty finding some good beginner material to start with. Would anyone be able to recommend some basics? </p>

CC BY-SA 3.0
2013-10-09T17:06:29.190Z
Have you checked the references in the Wikipedia article [proof complexity](http://en.wikipedia.org/wiki/Proof_complexity)? Steve and Phuong's book is relatively easy to read.
Kaveh
CC BY-SA 3.0
2013-10-09T17:10:39.260Z
I enjoyed the presentation given by Olaf Beyersdorff in Helsinki this summer. Check out [his slides here](http://satsmt2013.ics.aalto.fi/slides/Beyersdorff.pdf).
Juho
<cc.complexity-theory><lo.logic><proof-complexity>
Start learning proof complexity
Yugioh Mishima
# Start learning proof complexity

(Asked by: username_0 on 2013-10-09)

I recently started to read a lot about proof complexity and have been really enjoying what I have been reading. I would really like to learn more about this, but I am having difficulty finding some good beginner material to start with. Would anyone be able to recommend some basics?

**Tags:** cc.complexity-theory, lo.logic, proof-complexity
> **Comments:**
> **username_1**: Have you checked the references in the Wikipedia article [proof complexity](http://en.wikipedia.org/wiki/Proof_complexity)? Steve and Phuong's book is relatively easy to read.  
> **username_2**: I enjoyed the presentation given by Olaf Beyersdorff in Helsinki this summer. Check out [his slides here](http://satsmt2013.ics.aalto.fi/slides/Beyersdorff.pdf).  

---

## 4 answers

### Answer by username_3 on 2013-10-10. Score: 13

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).

> **Comments:**
> **username_0**: Thank you very much! I will dig in to these and see how they turn out  

---

### Answer by username_4 on 2013-10-11. Score: 6

I find these introductory lecture notes easy to read: [Paul Beame's IAS Lectures](http://www.cs.cornell.edu/~sabhar/publications/iaspcmi-proofcomplexity00.pdf)

> **Comments:**
> **username_5**: 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](http://www.csc.kth.se/~jakobn/research/PhDthesis.pdf)).  

---

### Answer by username_6 on 2013-10-10. Score: 6

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

* T. Pitassi. [Algebraic propositional proof systems](http://www.cs.toronto.edu/~toni/Papers/pitassi-algebraic.ps), 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:

* Clegg, Matthew; Edmonds, Jeffery; Impagliazzo, Russell. [Using the Groebner basis algorithm to find proofs of unsatisfiability](http://dx.doi.org/10.1145/237814.237860) STOC 1996, 174-183. (Also available from author's webpages without paywall.)


---

### Answer by username_5 on 2013-10-28. Score: 5

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).


---

