Feasible Proofs of Matrix Properties with Csanky’s Algorithm

  • Michael Soltys
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


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 \(\textbf{AC}^0[2]\subsetneq\textbf{DET}(\text{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).


Proof complexity Csanky’s algorithm matrix algebra 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bonet, M., Buss, S., Pitassi, T.: Are there hard examples for Frege systems? Feasible Mathematics II, 30–56 (1994)Google Scholar
  2. 2.
    Cook, S., Urquhart, A.: Functional interpretations of feasible constructive arithmetic. Annals of Pure and Applied Logic 63, 103–200 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Cook, S.A.: A taxonomy of problems with fast parallel algorithms. Information and Computation 64(13), 2–22 (1985)zbMATHGoogle Scholar
  4. 4.
    Grädel, E.: Capturing complexity classes by fragments of second-order logic. Theoretical Computer Science 101(1), 35–57 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Razborov, A.A.: Lower bounds on the size of bounded depth networks over a complete basis with logical addition. Mathematicheskie Zametki 41, 598–607 (1987); English translation in Mathematical Notes of the Academy of Sciences of the USSR 41, 333–338 (1987)MathSciNetGoogle Scholar
  6. 6.
    Smolensky, R.: Algebraic methods in the theory of lower bounds for Boolean circuit complexity. In: Proceedings, 19th ACM Symposium on Theory of Computing, pp. 77–82 (1987)Google Scholar
  7. 7.
    Soltys, M.: The Complexity of Derivations of Matrix Identities. PhD thesis, University of Toronto (2001)Google Scholar
  8. 8.
    Soltys, M., Cook, S.: The complexity of derivations of matrix identities. Annals of Pure and Applied Logic 130, 277–323 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Spence, L.E., Insel, A.J., Friedberg, S.H.: Elementary Linear Algebra: A Matrix Approach. Prentice-Hall, Englewood Cliffs (1999)Google Scholar
  10. 10.
    Thapen, N., Soltys, M.: Weak theories of linear algebra. Archive for Mathematical Logic 44(2), 195–208 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    von zur Gathen, J.: Parallel linear algebra. In: Reif, J.H. (ed.) Synthesis of Parallel Algorithms, pp. 574–617. Morgan and Kaufman, San Francisco (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Michael Soltys
    • 1
  1. 1.Computing and SoftwareMcMaster UniversityHamiltonCanada

Personalised recommendations