We initiate the study of the tradeoff between the {\em length} of a
probabilistically checkable proof of proximity (PCPP) and the
maximal {\em soundness} that can be guaranteed by a $3$-query
verifier with oracle access to the proof. Our main observation is
that a verifier limited to querying a short ... more >>>

We show that tree-like OBDD proofs of unsatisfiability require an exponential increase ($s \mapsto 2^{s^{\Omega(1)}}$) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase ($s \mapsto 2^{ 2^{\left( \log s \right)^{\Omega(1)}}}$) in proof size to simulate $\Res{O(\log n)}$. The ``OBDD proof ... more >>>

For any given Boolean formula $\phi(x_1,\dots,x_n)$, one can
efficiently construct (using \emph{arithmetization}) a low-degree
polynomial $p(x_1,\dots,x_n)$ that agrees with $\phi$ over all
points in the Boolean cube $\{0,1\}^n$; the constructed polynomial
$p$ can be interpreted as a polynomial over an arbitrary field
$\mathbb{F}$. The problem ... more >>>