Topics in propositional proof complexity
Leszek Kołodziejczyk (University of Warsaw).
Course Summary |
About the lecturer |
Location and schedule |
Materials |
Videos
|
Assignment
Propositional proof complexity studies how hard it is to prove tautologies in various proof systems for propositional logic. The original motivation for this field was the hope that it could contribute to solving the NP vs coNP problem. More recently, proof complexity has also come to be seen as a tool that provides a theoretical understanding of the limitations of modern-day SAT-solvers.
This course will present a sampling of ideas and results in proof complexity, aimed at somebody who has some very basic familiarity with logic and computational complexity but has never been introduced to proof complexity as such. Over the years the area has become highly combinatorial, but I will emphasize arguments that are not too involved and are at least partly inspired by ideas from logic. We will focus mostly on a relatively weak but extremely important proof system known as resolution. One of the results that I would like to cover is the recent theorem of Atserias and Müller (best paper at FOCS 2019) that resolution does not have a desirable property known as automatability unless P=NP.
About the lecturer:Leszek Kołodziejczyk is a mathematician who works on problems in the theory of computation from the perspective of mathematical logic. Among other things, his results give bounds on the strength of the axioms of arithmetic or set theory needed to establish eminent theorems like Fermat's Last Theorem or determinacy theorems used in automata theory. This approach also sheds new light on open problems in computational complexity theory. Leszek Kołodziejczyk has published in prestigious mathematical logic journals, but also in the topmost conferences in theoretical computer science like LICS and FOCS.
Location and schedule:ZOOM, link received upon registration. The videos will be recorded and posted here after each lecture.
|
|
|
||||||||||||||||||