Moscow Mathematical Journal 2(4): 647-679, 2002.

**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

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

Back to the list of papers