Feasible Proofs of Matrix Properties with Csanky's Algorithm
| dc.creator | Soltys, Michael | |
| dc.date | 2005-05-31 | |
| dc.date.accessioned | 2026-07-07T03:23:04Z | |
| dc.date.available | 2026-07-07T03:23:04Z | |
| dc.description | 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). | |
| dc.identifier | https://arxiv.org/abs/cs/0505087 | |
| dc.identifier | http://arxiv.org/abs/cs/0505087 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/32799 | |
| dc.subject | Logic in Computer Science | |
| dc.title | Feasible Proofs of Matrix Properties with Csanky's Algorithm | |
| dc.type | text |