Abstract
Let P be a sound proof system for propositional logic. For each CNF formula F, let SAT(F) be a CNF formula whose satisfying assignments are in 1to1 correspondence with those of F (e.g., F itself). For each integer s, let REF(F,s) be a CNF formula whose satisfying assignments are in 1to1 correspondence with the Prefutations of F of length s. Since P is sound, it is obvious that the conjunction formula SAT(F) & REF(F,s) is unsatisfiable for any choice of F and s. It has been long known that, for many natural proof systems P and for the most natural formalizations of the formulas SAT and REF, the unsatisfiability of SAT(F) & REF(F,s) can be established by a short refutation. In addition, for many P, these short refutations live in the proof system P itself. This is the case for all Frege proof systems. In contrast it was known since the early 2000’s that Resolution proofs of Resolution’s soundness statements must have superpolynomial length. In this talk I will explain how the soundness formulas for a proof system P relate to the computational complexity of the proof search problem for P. In particular, I will explain how such formulas are used in the recent proof that the problem of approximating the minimum prooflength for Resolution is NPhard (AtseriasMüller 2019). Besides playing a key role in this hardness of approximation result, the renewed interest in the soundness formulas led to a complete answer to the question whether Resolution has subexponentiallength proofs of its own soundness statements (Garlík 2019).
BibTeX  Entry
@InProceedings{atserias:LIPIcs:2020:13243,
author = {Albert Atserias},
title = {{Proofs of Soundness and Proof Search (Invited Talk)}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {2:12:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771740},
ISSN = {18688969},
year = {2020},
volume = {182},
editor = {Nitin Saxena and Sunil Simon},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13243},
URN = {urn:nbn:de:0030drops132439},
doi = {10.4230/LIPIcs.FSTTCS.2020.2},
annote = {Keywords: Proof complexity, automatability, Resolution, proof search, consistency statements, lower bounds, reflection principle, satisfiability}
}
Keywords: 

Proof complexity, automatability, Resolution, proof search, consistency statements, lower bounds, reflection principle, satisfiability 
Collection: 

40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020) 
Issue Date: 

2020 
Date of publication: 

04.12.2020 