BEGIN:VCALENDAR
VERSION:2.0
PRODID:www.ai.lu.se
BEGIN:VEVENT
UID:61e7d112df455
DTSTART:20211025T120000Z
SEQUENCE:0
TRANSP:OPAQUE
DTEND:20211025T140000Z
LOCATION:Online - link by registration
SUMMARY:MIAO video seminar: Proof complexity lower bounds by composition
CLASS:PUBLIC
DESCRIPTION:Contact: jakob.nordstrom@cs.lth.se\n\nTitle: \;Proof comple
xity lower bounds by composition\n\nSpeaker: Robert Robere\, McGill Univer
sity\n\nHost: Jacob NordstrÃ¶m\, \;Department of Computer Science\, Lu
nd University Joint with\n\nWhere: Online - link by registration\n\nAbstra
ct\n\nIn recent years\, there has been an explosion in the development of
so-called \"lifting theorems\" in proof complexity and other closely relat
ed areas which have led to the resolution of many long-standing open probl
ems. The basic idea of a lifting theorem is simple: in order to prove a lo
wer bound in a \"complicated\" system that we do not understand (for examp
le\, Cutting Planes refutations)\, we will \"escalate\" the hardness from
a \"simple\" system that we do understand (for example\, Resolution refuta
tions) by taking a hard formula F for the simple system and composing it w
ith a specially chosen \"gadget function\" that removes the power of the c
omplicated system. In many cases\, it is possible to prove that the \"best
\" possible strategy in the complicated system for refuting the composed f
ormula is to simulate the proof of the uncomposed formula in the simple sy
stem (and thus lower bounds for the uncomposed formula are \"escalated\" o
r \"lifted\" to lower bounds for the composed formula). While lifting theo
rems in circuit complexity can be traced back to the work of Raz and McKen
zie [RM99]\, recent developments have pushed these techniques to many new
areas\, and have shown how lifting is a flexible tool that allows quite fi
nely tuned tradeoffs between different parameters for a wide variety of pr
oof systems.\n\nIn this talk\, we give an introduction to and survey of li
fting results in proof complexity and related fields\, like communication
complexity and circuit complexity\, and outline some of the ways that lift
ing can be used to control various \"complexity parameters\" of unsatisfia
ble CNF formulas (like proof length\, proof space\, proof depth\, etc.). W
e will highlight several recent developments in the area and indicate some
future directions.\n\nPlease register at lth.se/digitalth/events/register
\;in order to get an access link to the zoom platform.\n\n\nThe MIAO
video seminars are arranged by the \;Mathematical Insights into Algor
ithms for Optimization (MIAO) \;research group at the University of Co
penhagen and Lund University. Most of our seminars consist of two parts: f
irst a 50-55-minute regular talk\, and then after a break an optional ca-1
-hour in-depth technical presentation with (hopefully) a lot of interactio
n. The intention is that the first part of the seminar will give all liste
ners a self-contained overview of some exciting research results. For list
eners who are particularly interested\, there is then an opportunity to re
turn for a second part where we get into more technical details.\n\n\nMore
information about the event: https://www.ai.lu.se/2021-10-25b
DTSTAMP:20220119T085130Z
END:VEVENT
END:VCALENDAR