Algebraic Proof Complexity

Iddo Tzameret, Royal Holloway, University of London. Part of the algebra, logic and algorithms seminar series.

This talk is dedicated to emerging connections between proof-size lower bounds on strong propositional proof systems such as Frege and lower bounds on the size of algebraic circuits.

First, I will show that lower bounds on Frege proofs follow from certain size lower bounds on a fairly weak model of computation, namely, non-commutative algebraic formulas. For this weak model of computation, many strong size lower bounds are already known since the early 90s. The argument is a characterization of propositional proofs as non-commutative formulas.

Then, I will discuss how lower bounds techniques from algebraic circuit complexity yield almost directly lower bounds on the proof-size of fairly strong systems such as Nullstellensatz and the Ideal Proof System, when refutations in both systems are written as algebraic circuits taken from some restricted circuit classes.

I will conclude with some open questions related to advancing the frontiers of algebraic proof complexity.

Iddo TzameretRoyal Holloway, University of London