We consider two well-known algebraic proof systems: Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr), a system introduced in \cite{abrw02j} which combines together Pc and Resolution.
Moreover we introduce an algebraic proof system Pcr{k}, which combines together Polynomial Calculus Pc and k-DNF Resolution (Res{k}).
This is a natural generalization to Res{k} of Pcr.
In the paper we study the complexity of proofs in such systems.
First we prove that a set of polynomials encoding a Graph Ordering Principle (Gop(G)) requires Pcr refutations of degree $\Omega(n)$. This is the first linear degree lower bound for \Pcr\ refutations for ordering principles. This result immediately implies that the size-degree tradeoff for Pcr Refutations of Alekhnovich et al. \cite{abrw04j} is optimal, since there are polynomial size Pcr refutations for Gop(G).
We then study the complexity of proofs in Pcr{k}, extending to these systems the lower bounds known for Res{k}:
- we prove that random $3$-CNF formulas with a linear number of clauses are hard to prove in Pcr{k} (over a field with characteristic different from $2$) as long as $k$ is in $o(\sqrt{\log n/\log \log n})$. This is the strongest daglike system where $3$-CNF formulas are hard to prove.
- Moreover we prove a strict hierarchy result showing that \Pcrk{k+1} is
exponentially stronger than Pcr{k}.
We introduce an algebraic proof system Pcrk, which combines together {\em Polynomial Calculus} (Pc) and {\em $k$-DNF Resolution} (Resk).
This is a natural generalization to Resk of the well-known {\em Polynomial Calculus with Resolution} (Pcr) system which combines together Pc and Resolution.
We study the complexity of proofs in such a system extending to Pcrk the results known for Resk. We prove that random 3-CNF formulas with a linear number of clauses are hard to prove in Pcrk (over a field with characteristic different from 2) as long as k is in $o(\sqrt{\log n/\log \log n})$. This is the strongest system where 3-CNF formulas are hard to prove.
Moreover we prove a strict hierarchy result showing that Pcr(k+1) is exponentially stronger than Pcrk. This result is the consequence of proving a $\Omega(n)$ degree lower bound for Pcr refutations of a {\em Graph Ordering Principle}. This is the first example of a family of contradictions having Pcr short refutations but requiring high degree, and thus also proving the optimality of the size-degree tradeoff for Pcr.