[Proof Complexity] Seminar Mon Oct 25 at 14:00 CEST with Robert Robere: Proof complexity lower bounds by composition

[Jakob Nordström]

Dear all,

On Monday October 25 at 14:00 CEST we will have a MIAO video seminar with Robert Robere from McGill University titled "Proof complexity lower bounds by composition". See below for the abstract.

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 have the additional 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.jakobnordstrom.se/videoseminars/ . In particular, on Friday October 15 at 10:00 we are having a seminar "Logic-based explainable AI" with Alexey Ignatiev from Monash University, and on Friday October 22 at 14:00 it is time for the seminar "Verified proof checkers" with Magnus Myreen from Chalmers University of Technology. 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 Oct 25 at 14:00 CEST
Proof complexity lower bounds by composition
(Robert Robere, McGill University)

In recent years, there has been an explosion in the development of so-called "lifting theorems" in proof complexity and other closely related areas which have led to the resolution of many long-standing open problems. The basic idea of a lifting theorem is simple: in order to prove a lower bound in a "complicated" system that we do not understand (for example, Cutting Planes refutations), we will "escalate" the hardness from a "simple" system that we do understand (for example, Resolution refutations) by taking a hard formula F for the simple system and composing it with a specially chosen "gadget function" that removes the power of the complicated system. In many cases, it is possible to prove that the "best" possible strategy in the complicated system for refuting the composed formula is to simulate the proof of the uncomposed formula in the simple system (and thus lower bounds for the uncomposed formula are "escalated" or "lifted" to lower bounds for the composed formula). While lifting theorems in circuit complexity can be traced back to the work of Raz and McKenzie [RM99], recent developments have pushed these techniques to many new areas, and have shown how lifting is a flexible tool that allows quite finely tuned tradeoffs between different parameters for a wide variety of proof systems.

In this talk, we give an introduction to and survey of lifting results in proof complexity and related fields, like communication complexity and circuit complexity, and outline some of the ways that lifting can be used to control various "complexity parameters" of unsatisfiable CNF formulas (like proof length, proof space, proof depth, etc.). We will highlight several recent developments in the area and indicate some future directions.


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