A propositional proof system (Cook and Reckhow, 1977) is a polynomial time computable predicate S such that a propositional formula F is unsatisfiable iff there exists a proof p for which S(F, p) holds. In other words, it is an efficient (in the size of the proof) procedure to check the correctness of proofs presented in a certain format. Finding short proofs, however, may still be difficult. In fact, short proofs may not exist in the proof system if it is too weak. In the rest of this paper, we refer to such systems simply as proof systems and omit the word propositional.