“Non-logical” proofs of logical formulas

The problem whether a propositional formula is provable is one of the most computationally “easy” problems in the proof theory. Nevertheless, it is a very important problem, because it is closely related to the celebrated P vs NP question (one of the seven questions for which Clay Mathematics Institute offers a \$1,000,000 prize). Namely, if there is no propositional proof system in which every tautology has a polynomial-size proof, then NP!=co-NP (hence, P!=NP).
Naturally, no such fact is proved for any of the known proof systems, though for some of them negative results (exponential lower bounds) are known. During the past decade, not only “pure logical” proof systems attracted researchers, but also (and mainly) other systems, e.g., “algebraic” systems (which work with polynomials instead of logical formulas). Interesting systems arise also from the derandomization of probabilistic algorithms: such derandomization frequently uses, e.g., coding theory or projective geometry.
In the talk I will survey various propositional proof systems.