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.