Algebraic Proof Complexity
- Date: Wednesday 22 March 2017, 16:00 – 17:30
- Location: Mathematics Level 8, MALL 1 & 2, School of Mathematics
- Type: Algebra, Logic and Algorithms, Logic, Seminars, Pure Mathematics
- Cost: Free
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 Tzameret, Royal Holloway, University of London