Linear Lower Bound on Degrees of Positivstellensatz Calculus Proofs for the211 Parity

摘要

It is established a linear (thereby, sharp) lower bound on degrees of211u001ePositivstellensatz calculus refutations introduced in (GV99), for the Tseitin 211u001etautologies and for the parity (the mod 2 principle). We use the machinery of the 211u001eLaurent proofs developed for binomial systems in (BuGI 98), (GuGI 99).