Complexity of Propositional Proofs (Invited Talk)

摘要

The underlying question of propositional proof complexity is amazingly simple: when interesting propositional tautologies possess efficient (which usually means short) proofs in a given propositional proof system? This theory is extremely well connected to very different disciplines like computational complexity, theoretical cryptography, automated theorem proving, mathematical logic, algebra and geometry. And, given its mixed origins, methods and concepts employed in the area are also very diverse. In this lecture we will try to accomplish as much of the following as possible; our choice of topics is highly biased and personal.