Weak theories of linear algebra |
| |
Authors: | Neil Thapen Michael Soltys |
| |
Affiliation: | (1) St Hildas College, Cowley Place, Oxford, OX4 1DY, UK;(2) Department of Computing and Software, McMaster University, 1280 Main Street West, Hamilton, Ontario, L8S 4K1, Canada |
| |
Abstract: | We investigate the theories of linear algebra, which were originally defined to study the question of whether commutativity of matrix inverses has polysize Frege proofs. We give sentences separating quantified versions of these theories, and define a fragment in which we can interpret a weak theory V1 of bounded arithmetic and carry out polynomial time reasoning about matrices - for example, we can formalize the Gaussian elimination algorithm. We show that, even if we restrict our language, proves the commutativity of inverses.This work was done while a postdoctoral research fellow at the Department of Computer Science, University of Toronto, Canada. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|