Complexity of semi-algebraic proofs

Proof systems for polynomial inequalities in 0-1 variables include the well-studied Cutting Planes proof system (CP) and the Lov´asz-Schrijver calculi (LS) utilizing linear, respectively, quadratic, inequalities. We introduce generalizations LS^d of LSinvolving polynomial inequalities of degree at most d.Surprisingly, the systems LS^d turn out to be very strong. We construct polynomial-size bounded degree LS^d proofs of the clique-coloring tautologies (which have no polynomial-size CP proofs), the symmetric knapsack problem (which has no bounded degree Positivstellensatz Calculus (PC) proofs), and Tseitin’s tautologies (hard for many known proof systems). Extending our systems with a division rule yields a polynomial simulation of CP with polynomially bounded coefficients, while other extra rules further reduce the proof degrees for the aforementioned examples. Finally, we prove lower bounds on Lov´asz-Schrijver ranks, demonstrating, in particular, their rather limited applicability for proof complexity.