Fall 2018

Lower Bounds Techniques in Proof Complexity I

Tuesday, August 21st, 2018 9:30 am10:30 am

Add to Calendar

I will talk about the broad field of proof complexity. Its central question is whether there exists an NP algorithm certifying that a Boolean formula is unsatisfiable. Or, put differently, whether there exists a propositional
proof system P in which every unsatisfiable formula has a short refutation. The expected answer is ”no”, but this can be unconditionally proved only for relatively weak systems P, such as Resolution, Cutting Planes, or bounded-depth Frege. I will overview techniques used in the area, as well as focus on open problems.