An Isaac Newton Institute Workshop

New Directions in Proof Complexity

The proof complexity of matrix algebra

Author: M Soltys (McMaster University)

Abstract

There are fast parallel algorithms for computing the characteristic polynomial of a matrix: notably Berkowitz's and Csanky's algorithms. While these algorithms run in NC2, all the known proofs of correctness require polynomial time concepts. Are there quasi-polynomial Frege (i.e., NC2-Frege) proofs of correctness of these algorithms? Or is it the case the universal matrix identities separate Frege and Extended Frege? This talk will address these questions and present recent progress in this area.