[Proof Complexity] Seminar Mon Jun 7 at 14:00 CEST with Joanna Ochremiak: Proof complexity meets finite model theory

[Jakob Nordström]

Dear all,

On Monday June 7 at 14:00 CEST we will have a seminar with Joanna Ochremiak from Université de Bordeaux and CNRS titled "Proof complexity meets finite model theory". Please see the abstract below for more details.

We will meet 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 video seminars can be found at http://www.csc.kth.se/~jakobn/videoseminars/ (an address that should change soonish, but for now it is what it is). In particular, please note that we also have a seminar on Friday June 4 at 14:00 CEST with Jeremias Berg titled "Abstract cores in implicit hitting set based MaxSAT solving".

If you do not wish to receive these announcements, or receive several copies of them, please send a message to jakob.nordstrom at cs.lth.se.

Best regards,
Jakob Nordström

**********

Monday Jun 7 at 14:00 CEST
Proof complexity meets finite model theory
(Joanna Ochremiak, LaBRI, Université de Bordeaux and CNRS)

Finite model theory studies the power of logics on the class of finite structures. One of its goals is to characterize symmetric computation, that is, computation that abstracts away details which are not essential for the given task, by respecting the symmetries of the input.

In this talk I will discuss connections between proof complexity and finite model theory, focussing on lower bounds. For certain proof systems, the existence of a succinct refutation can be decided in a symmetry-preserving way. This allows us to transfer lower bounds from finite model theory to proof complexity. I will introduce this approach and explain its key technical ideas such as the method of folding for dealing with symmetries in linear programs.

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