Exponential lower bound for static semi-algebraic proofs.
Hirsch, Edward A.
Pasechnik, Dmitrii V.
Date of Issue2002
School of Physical and Mathematical Sciences
Semi-algebraic proof systems were introduced in  as extensions of Lovász-Schrijver proof systems [2,3]. These systems are very strong; in particular, they have short proofs of Tseitin’s tautologies, the pigeonhole principle, the symmetric knapsack problem and the clique-coloring tautologies . In this paper we study static versions of these systems. We prove an exponential lower bound on the length of proofs in one such system. The same bound for two tree-like (dynamic) systems follows. The proof is based on a lower bound on the “Boolean degree” of Positivstellensatz Calculus refutations of the symmetric knapsack problem.
Automata, languages and programming
© 2002 Springer. This is the author created version of a work that has been peer reviewed and accepted for publication by Automata, Languages and Programming, Springer. It incorporates referee’s comments but changes resulting from the publishing process, such as copyediting, structural formatting, may not be reflected in this document. The published version is available at: [DOI:https://dx.doi.org/10.1007/3-540-45465-9_23].