[Proof Complexity] Seminar Wednesday Oct 5 at 14:00 CET with Susanna F. de Rezende: Theoretical barriers for efficient proof search

[Jakob Nordström]

Dear all,

It is a privilege to invite you to our seminar on Wednesday October 5 at 14:00 CET with Susanna F. de Rezende, our (perhaps already not so) new assistant professor in theoretical computer science at Lund University. Susanna's talk is titled "Theoretical barriers for efficient proof search", and you find the abstract at the bottom of this message.

We will run this as a hybrid seminar at Lund University. Local participants are welcome to seminar room E:2116 at Ole Römers väg 3. Other participants are invited to join virtually at https://lu-se.zoom.us/j/61925271827. Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners an overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming MIAO seminars can be found at http://www.jakobnordstrom.se/miao-seminars/. In particular, don't miss the seminars with Albert Atserias on Friday this week and Robert Andrews on Tuesday next week! If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

Wednesday Oct 5 at 14:00 in seminar room E:2116, Ole Römers väg 3, Lund University, and on Zoom
Theoretical barriers for efficient proof search
(Susanna F. de Rezende, Lund University)

The proof search problem is a central question in automated theorem proving and SAT solving. Clearly, if a propositional tautology F does not have a short (polynomial size) proof in a proof system P, any algorithm that searches for P-proofs of F will necessarily take super-polynomial time. But can proofs of "easy" formulas, i.e., those that have polynomial size proofs, be found in polynomial time? This question motivates the study of automatability of proof systems. In this talk, we give an overview of known non-automatability results, focusing on the more recent ones, and present some of the main ideas used to obtain them.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se