Logic in Computer Science (LICS 2002)

Paper: The Proof Complexity of Linear Algebra (at LICS 2002)

Authors: Michael Soltys Stephen Cook

Abstract

We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley-Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities.

BibTeX

  @InProceedings{SoltysCook-TheProofComplexityo,
    author = 	 {Michael Soltys and Stephen Cook},
    title = 	 {The Proof Complexity of Linear Algebra},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }