Abstract. It is a known approach to translate propositional formulas into systems of polynomial inequalities and to consider proof systems for the latter ones. The well-studied proof systems of this kind are the Cutting Planes proof system (CP) utilizing linear inequalities and the Lovász-Schrijver calculi (LS) utilizing quadratic inequalities. We introduce generalizations LS^d of LS that operate with polynomial inequalities of degree at most d.

It turns out that the obtained proof systems are 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 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 the aforementioned examples.

Finally, we prove lower bounds on Lovász-Schrijver ranks and on the "Boolean degree" of Positivstellensatz Calculus refutations. We use the latter bound to obtain an exponential lower bound on the size of static LS^d and tree-like LS^d refutations.

[ Full text (draft version): .ps.gz ]