Analyzing refutations of the well known
pebbling formulas we prove some new strong connections between pebble games and algebraic proof system, showing that
there is a parallelism between the reversible, black and black-white pebbling games on one side, and
the three algebraic proof systems NS, MC and PC on the other side. In particular we prove:
\begin{itemize}
\item For any DAG $G$ with a single sink, if there is a Monomial Calculus refutation
for $Peb(G)$ having simultaneously degree $s$ and size $t$
then there is a black pebbling strategy on $G$ with space $s$ and time $t+s$.
Also if there is a black pebbling strategy for $G$ with space $s$ and time $t$ it is possible to extract from it
a MC refutation
for $Peb(G)$ having simultaneously degree $s$ and size $2t(s-1)$.
These results are analogous to those proven in [de Rezende et al. 21] for the case of reversible pebbling and
Nullstellensatz.
Using them we prove degree separations between NS and MC
as well as strong degree-size tradeoffs for MC.
\item We show that the variable space needed for the refutation of pebbling formulas in Polynomial Calculus exactly
coincides with the black-white pebbling number of the corresponding graph.
One direction of this result was known. We present an new elementary proof of it.
\item
We show that for any unsatisfiable CNF formula $F,$ the variable space in a Resolution refutation
of the formula is a lower bound for the monomial space in a PCR refutation for
the extended formula $F[\oplus]$.
This implies that
for any DAG
$G$, the monomial space needed in the PCR refutation of an XOR pebbling formulas is lower bounded
by the black-white pebbling number of the corresponding graph. This solves affirmatively Open Problem 7.11 from
[Buss Nordström 21].
\item
The last result
also
proves a strong separation between degree and monomial space in PCR of size $\Omega(\frac{n}{\log n})$
with the additional property
that it is independent of the field characteristic. This question
was posed in [Filmus et al. 13].
\end{itemize}
We found out a mistake in the proof of Theorem 30, therefore we do not claim anymore that we have proven that for any unsatisfiable CNF formula F the variable space in a Resolution refutation
of the formula is a lower bound for the monomial space in a PCR refutation for
the extended formula $F[\oplus]$. This result is still open.
Also, we were pointed out that the result in Theorem 28 follows directly from known results
from [Ben09] and [BNT13] .