Feasible proofs of matrix properties with Csanky's algorithm
Academic Article

Overview

Research

Additional Document Info

View All

Overview

abstract

We show that Csanky's fast parallel algorithm for computing the
characteristic polynomial of a matrix can be formalized in the logical theory
LAP, and can be proved correct in LAP from the principle of linear
independence. LAP is a natural theory for reasoning about linear algebra
introduced by Cook and Soltys. Further, we show that several principles of
matrix algebra, such as linear independence or the Cayley-Hamilton Theorem, can
be shown equivalent in the logical theory QLA. Applying the separation between
complexity classes AC^0[2] contained in DET(GF(2)), we show that these
principles are in fact not provable in QLA. In a nutshell, we show that linear
independence is ``all there is'' to elementary linear algebra (from a proof
complexity point of view), and furthermore, linear independence cannot be
proved trivially (again, from a proof complexity point of view).