Iddo Tzameret

We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege--yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analogue of Frege proofs, different from that given in Buss ... more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

We define a cutting planes system CP+$\forall$red for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while ... more >>>

Johan HÃ¥stad

We prove that a small-depth Frege refutation of the Tseitin contradiction

on the grid requires subexponential size.

We conclude that polynomial size Frege refutations

of the Tseitin contradiction must use formulas of almost

logarithmic depth.

Fedor Part, Iddo Tzameret

Resolution over linear equations (introduced in [RT08]) emerged recently as an important object of study. This refutation system, denoted Res(lin$_R$), operates with disjunction of linear equations over a ring $R$. On the one hand, the system captures a natural ``minimal'' extension of resolution in which efficient counting can be achieved; ... more >>>