Title	Automated Proof Search: The Aftermath
Creator	Goos, Mika
Publisher	Banff International Research Station for Mathematical Innovation and Discovery
Date Issued	2020-01-22T11:11
Description	In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper) settled the complexity of finding short proofs in Resolution, the most basic propositional proof system. Namely, given an unsatisfiable CNF formula F, they showed it is NP-hard to find a Resolution refutation of F in time polynomial in the length of the shortest such refutation. In this talk, we present a simple proof of the Atserias--Muller theorem. The new proof generalises better: We obtain analogous hardness results for Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work) Cutting Planes. An open problem is to include Sum-of-Squares in this list. Based on joint works with Sajin Koroth, Ian Mertz, Jakob NordstrÃ¶m, Toniann Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.
Extent	46.0 minutes
Subject	Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science
Type	Moving Image
File Format	video/mp4
Language	eng
Notes	Author affiliation: Stanford University
Series	BIRS Workshop Lecture Videos (Banff, Alta)
Date Available	2020-07-21
Provider	Vancouver : University of British Columbia Library
Rights	Attribution-NonCommercial-NoDerivatives 4.0 International
DOI	10.14288/1.0392480
URI	http://hdl.handle.net/2429/75227
Affiliation	Non UBC
Peer Review Status	Unreviewed
Scholarly Level	Postdoctoral
Rights URI	http://creativecommons.org/licenses/by-nc-nd/4.0/
Aggregated Source Repository	DSpace

Open Collections

BIRS Workshop Lecture Videos

Automated Proof Search: The Aftermath Goos, Mika

Description

Item Metadata

Item Media

Item Citations and Data

Rights