Open Collections

Lifting in Proof Complexity

Banff International Research Station for Mathematical Innovation and Discovery

A growing number of results in proof complexity rely on so-called "lifting" techniques (also called hardness escalation"), which are inspired from communication complexity. In the context of proof complexity, the basic idea of lifting is simple: in order to prove lower bounds in a proof system that is complex", start with a formula F that is hard for a "simple" proof system, and make the formula F harder by replacing each variable in F with some inner function that is hard to represent in the "complex" system. Often, we are able to show that the best proof for the composed formula in the complex proof system is to simulate the proof in the simple system --- thus, this reduces the lower bound problem from the complex proof system to proving lower bounds in the simple system, which is often much easier. In this survey talk, we will give an introduction to these techniques, survey some of the applications, and delineate when the techniques can be applied. No prior background in lifting techniques or communication complexity will be necessary.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: Technion

2020-07-21

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/75225

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/