The proof-search problem between bounded-width resolution and bounded-degree semi-algebraic proofs

Abstract

In recent years there has been some progress in our understanding of the proof-search problem for very low-depth proof systems, e.g. proof systems that manipulate formulas of very low complexity such as clauses (i.e. resolution), DNF-formulas (i.e. R(k) systems), or polynomial inequalities (i.e. semi-algebraic proof systems). In this talk I will overview this progress. I will start with bounded-width resolution, whose specialized proof-search algorithm is as easy as uninteresting, but whose proof-search problem is unintentionally solved by certain versions of conflict-driven clause-learning algorithms with restarts. I will continue with R(k) systems, whose proof-search problem turned out to hide the complexity of certain two-player games of interest in the area of systems synthesis and verification. And I will close with bounded-degree semi-algebraic proof systems, whose proof-search problem turned out to hide the complexity of systems of linear equations over finite fields, among other problems. © 2013 Springer-Verlag.