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

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

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