Proof complexity - an introduction

Computer Science/Discrete Mathematics Seminar II
Topic:Proof complexity - an introduction
Speaker:Avi Wigderson
Affiliation:Herbert H. Maass Professor, School of Mathematics
Date:Tuesday, March 15
Time/Room:10:30am - 12:30pm/S-101
Video Link:

Proof systems pervade all areas of mathematics (often in disguise: e.g. Reidemeister moves is a sound and complete proof system for proving the equivalence of knots given by their diagrams). Proof complexity seeks to to understand the minimal *length* of proofs relative to the length of theorem proved, mainly for propositional proof systems. In this talk I plan to survey some of the main motivations and goals, results and challenges of proof complexity, as well as its connections with circuit complexity. I will then discuss in more detail the Resolution proof system (the most basic nontrivial proof system, prevalent in automated theorem provers and in hardware verification systems), and show exponential lower bounds on proof-length in this system. No special knowledge in this area will be assumed.