The proof complexity of matrix algebra
Seminar Room 1, Newton Institute
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.