[Proof Complexity] MIAO seminar Thu Oct 30 at 13:15 CET (note the time!): Proof complexity as a computational lens

[Jakob Nordström]

Dear all,

With apologies for the short notice, this Thursday October 30 at 13:15 CET /(note the time!) /there will be a seminar titled "Proof complexity as a computational lens" given by yours truly. You find the abstract at the bottom of this message.

We will run this as a MIAO hybrid seminar at Lund University. Local participants are warmly welcome to seminar room E:2116 at Ole Römers väg 3, while other participants are equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 .

This is expected to be a ca-2-hour tutorial-style seminar, which will double as the first introductory lecture of a seminar course with the same name that will be given in Copenhagen and Lund during the winter of 2025/26. The course will focus on the part of proof complexity that can also be used to analyze SAT solvers, Gröbner basis algorithms, 0-1 linear programming solvers, and other combinatorial solving algorithms. More about the course can be found at https://jakobnordstrom.se/teaching/proofcplx25/ , but please feel free to reach out if you are interested in information about, e.g., how to follow lectures remotely.

Please feel free to share this information with colleagues who you think might be interested. As usual, we are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ . 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

**********

/Thursday Oct 30 at 13:15 (note the time!) in seminar room E:2116, Ole Römers väg 3, Lund University, and on Zoom
*Proof complexity as a computational lens
*(Jakob Nordström, University of Copenhagen and Lund University)
/
This seminar will give an overview of proof complexity with a focus on "algorithmically relevant" proof systems that, besides offering interesting objects for mathematical study, can also be used to analyze real-world combinatorial solving algorithms. We will talk about proof systems [and corresponding algorithms] such as resolution [DPLL and conflict-driven clause learning SAT solving], Nullstellensatz and polynomial calculus [linear algebra and Gröbner basis computations], and cutting planes [pseudo-Boolean solving and 0-1 integer linear programming]. Time permitting, we will also discuss briefly proof systems such as Sherali-Adams and sum of squares [linear programming and semidefinite programming hierarchies], stabbing planes [0-1 ILP], and extended resolution [SAT pre- and inprocessing].


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se