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?
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:
Stasys Jukna, Extremal Combinatorics With Applications in Computer Science, 2001, Springer-Verlag, Section 4.8.
Eli Ben-sasson and Avi Wigderson, Short Proofs are Narrow - Resolution made Simple (2000), JACM.
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.
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).
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:
- Clegg, Matthew; Edmonds, Jeffery; Impagliazzo, Russell. Using the Groebner basis algorithm to find proofs of unsatisfiability STOC 1996, 174-183. (Also available from author's webpages without paywall.)
I find these introductory lecture notes easy to read: Paul Beame's IAS Lectures
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).