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 Lovasz-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 Lovasz-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 refutations.

This revision contains a proof of exponential lower bound on the
size of Positivstellensatz Calculus refutations as well.

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 Lovasz-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 Lovasz-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 refutations.

This revision contains a shorter self-contained proof of Theorem 8.1.
It also fixed typos in Theorem 3.1 and Lemma 8.2 of Revision 1.

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 Lovasz-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 Lovasz-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.

This revision contains a shorter self-contained proof of Theorem 8.1.

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 Lovasz-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 Lovasz-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 refutations.