The proof complexity of linear algebra
Proceedings - Symposium on Logic in Computer Science - Trang 335-344
Tóm tắt
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.
Từ khóa
#Linear algebra #Matrices #Polynomials #Computer science #Educational institutions #Parallel algorithms #Galois fields #Lagrangian functions #LogicTài liệu tham khảo
10.1007/978-1-4612-2566-9_3
10.1016/0020-0190(84)90018-8
von zur gathen, 1993, Parallel linear algebra, Synthesis of Parallel Algorithms, 574
arai, 1995, Tractability of cut-free Gentzen type propositional calculus with permutation inference
10.1017/CBO9780511529948
10.1016/S0019-9958(85)80041-3
cook, 1975, Feasibly constructive proofs and the propositional calculus, Proc 7th ACM Symp Theory Comput, 83
buss, 1986, Studies in proof theory, Bounded Arithmetic
10.1016/S0166-218X(99)00039-6
soltys, 2001, The Complexity of Derivations of Matrix Identities