We prove that Polynomial Calculus and Polynomial Calculus with Resolution are not automatizable, unless W[P]-hard problems are fixed parameter tractable by one-side error randomized algorithms. This extends to Polynomial Calculus the analogous result obtained for Resolution by Alekhnovich and Razborov (SIAM J. Computing, 38(4), 2008).

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 ... more >>>

We define a collection of Prover-Delayer games that characterize certain subsystems of resolution. This allows us to give some natural criteria which guarantee lower bounds on the resolution width of a formula, and to extend these results to formulas of unbounded initial width.

We also use games to give upper ... more >>>

We study the space complexity of refuting unsatisfiable random $k$-CNFs in
the Resolution proof system. We prove that for any large enough $\Delta$,
with high probability a random $k$-CNF over $n$ variables and $\Delta n$
clauses requires resolution clause space of
$\Omega(n \cdot \Delta^{-\frac{1+\epsilon}{k-2-\epsilon}})$,
for any $0<\epsilon<1/2$. For constant $\Delta$, ... more >>>

We show that an LK proof of size $m$ of a monotone sequent (a sequent

that contains only formulas in the basis $\wedge,\vee$) can be turned

into a proof containing only monotone formulas of size $m^{O(\log m)}$

and with the number of proof lines polynomial in $m$. Also we show

We study the complexity of proving the Pigeon Hole
Principle (PHP) in a monotone variant of the Gentzen Calculus, also
known as Geometric Logic. We show that the standard encoding
of the PHP as a monotone sequent admits quasipolynomial-size proofs
in this system. This result is a consequence of ... more >>>