The underlying question of propositional proof complexity is amazingly simple: when interesting propositional tautologies possess efficient proofs in a given (propositional) proof system? This theory makes an integral part of more general theory of feasible provability (not necessarily propositional), the latter being widely considered as the proof theory for the world of efficiently computable objects. Other motivations for studying complexity of propositional proofs come from algebra, automated theorem proving and, of course, computational (especially circuit) complexity.

Given its mixed origin, the methods currently employed in this area are also very diverse. In this introductory talk I will try to illustrate some of them and give the audience at least some feeling of the current state of the art in the area.

For more information about the Penn Logic and Computation Seminar, please see the seminar web page.