Ran Raz, Iddo Tzameret

We introduce an algebraic proof system that manipulates multilinear arithmetic formulas. We show that this proof system is fairly strong, even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, we show the following:

1. Algebraic proofs manipulating depth 2 multilinear arithmetic formulas polynomially simulate Resolution, Polynomial ... more >>>

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

Iddo Tzameret, Stephen Cook

Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over $GF(2)$ in Hrubes-Tzameret [SICOMP'15]. Specifically, we show that the multiplicativity of the determinant function and the ... more >>>

Nashlen Govindasamy, Tuomas Hakoniemi, Iddo Tzameret

We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\sum_{i,j,k,l\in[n]} z_{ijkl}x_ix_jx_kx_l-\beta = 0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as ... more >>>