The Taub Faculty of Computer Science Events and Talks

The so called Extended Frege system is one of the most natural propositional proof systems. Whereas we believe that there exist tautologies which require exponential Extended Frege proofs, the best known lower bound is linear. To find even a modestly superlinear lower bound is a challenging open problem. I will discuss a possible approach to this question, which is based on counting the number of commutativity axioms in an Extended Frege proof, which in turn can be phrased as an algebraic problem about non-commutative polynomials. We will see that this line of reasoning generates new difficult questions, rather than answering the original one.