Feasible Proofs of Matrix Properties with Csanky's Algorithm

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 in [8]. 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 AC0 [2] 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). Key words: Proof complexity, Csanky’s algorithm, matrix algebra.

• Type: Conference
• Year: 2005
• Where: CSL
• Authors: Michael Soltys
• Keywords: CSL 2005, Linear Algebra, Linear Independence, Proof Complexity