Complexity of semialgebraic proofs

It is a known approach to translate propositional formulas into systems of polynomial inequalities and consider proof systems for the latter. The well-studied proof systems of this type are the Cutting Plane proof system (CP) utilizing linear inequalities and the Lovász–Schrijver calculi (LS) utilizing quadratic inequalities. We introduce generalizations ${\rm LS}^d$ of LS that operate on polynomial inequalities of degree at mos $d$.
It turns out that the obtained proof systems are very strong. We construct polynomial-size bounded-degree ${\rm 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 proofs), and Tseitin's tautologies (which are 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 those examples.
Finally, we prove lower bounds on the Lovász–Schrijver ranks and on the size and the “Boolean degree” of Positivstellensatz calculus refutations. We use the latter bound to obtain an exponential lower bound on the size of Positivstellensatz calculus,
textit{static} ${\rm LS}^d$, and tree-like ${\rm LS}^d$ refutations.