用Csanky算法证明矩阵性质
Feasible Proofs of Matrix Properties with Csanky's Algorithm
摘要：
我们证明了Csanky的快速并行算法计算的特征多项式的矩阵可以形式化的逻辑理论，并可以证明正确的线性无关性原则的逻辑理论。线性代数是由Cook和Soltys提出的一种自然推理理论。此外，我们表明，矩阵代数的几个原则，如线性无关性或凯莱-汉密尔顿定理，可以证明等价的逻辑理论QLA。应用DET（GF（2））中包含的复杂性类AC^0[2]之间的分离，我们证明了这些原则实际上在QLA中是不可证明的。简而言之，我们证明了线性独立性是初等线性代数的“全部”（从证明复杂性的角度来看），而且，线性独立性不能被简单地证明（再次，从证明复杂性的角度来看）。
英文摘要：
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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
