Journal article:

    Samuel R. Buss.
    "Propositional Proof Complexity: An Introduction."
    in Computational Logic, edited by U. Berger and H. Schwichtenberg.
    Springer-Verlag, Berlin, 1999, pp. 127-178.

    Download article: postscript or PDF. 

    Abstract: This is an introduction to propositional proof complexity. The main topics covered include Frege systems, abstract propositional proof systems, connections to computational complexity, resolution, the propositional pigeon-hole principle, extended Frege and substitution Frege proof systems, Craig interpolation for propositional logic, effective Craig interpolation for resolution, applications from monotone circuit complexity, cutting planes proof systems, normal forms for cutting planes proofs, Craig interpolation for cutting planes proof systems, and applications with monotone real circuits.