Running a SAT solver on an UNSAT formula produces (implicitly or explicitly) a proof that the formula is unsatisfiable, usually expressible in an established formal language called proof system. This observation leads to study SAT solving methods by looking at the generated proofs. I.e., if an UNSAT formula has no short proof in a given proof system, the corresponding SAT solvers cannot solve the formula efficiently. We introduce the area and the methods of proof complexity, that studies the length and the structure of proofs of UNSAT. In particular we define and discuss Resolution, Polynomial Calculus, Cutting Planes and Extended Resolution, which are the most relevant proof systems for current SAT solver technology. Since a SAT solver goal is, among other things, to look for proofs as short as possible, we briefly discuss the complexity of efficiently finding such short proofs.