Switch to: References

Citations of:

The proof complexity of linear algebra

Michael Soltys & Stephen Cook

Annals of Pure and Applied Logic 130 (1-3):277-323 (2004)

Add citations

You must login to add citations.

Proving properties of matrices over \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb{Z}_{2}}$$\end{document}. [REVIEW]Michael Soltys - 2012 - Archive for Mathematical Logic 51 (5-6):535-551.details We prove assorted properties of matrices over \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb{Z}_{2}}$$\end{document}, and outline the complexity of the concepts required to prove these properties. The goal of this line of research is to establish the proof complexity of matrix algebra. It also presents a different approach to linear algebra: one that is formal, consisting in algebraic manipulations according to the axioms of a ring, rather than the traditional semantic approach via linear transformations. Download Export citation Bookmark
The proof complexity of linear algebra.Michael Soltys & Stephen Cook - 2004 - Annals of Pure and Applied Logic 130 (1-3):277-323.details 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 such as AB=I→BA=I. Download Export citation Bookmark 8 citations
Short propositional refutations for dense random 3CNF formulas.Sebastian Müller & Iddo Tzameret - 2014 - Annals of Pure and Applied Logic 165 (12):1864-1918.details Download Export citation Bookmark 3 citations
Weak theories of linear algebra.Neil Thapen & Michael Soltys - 2005 - Archive for Mathematical Logic 44 (2):195-208.details 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 V 1 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. (shrink) Download Export citation Bookmark 2 citations
(1 other version)The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.details Propositional proof complexity is the study of the sizes of propositional proofs, and more generally, the resources necessary to certify propositional tautologies. Questions about proof sizes have connections with computational complexity, theories of arithmetic, and satisfiability algorithms. This is article includes a broad survey of the field, and a technical exposition of some recently developed techniques for proving lower bounds on proof sizes. Download Export citation Bookmark 17 citations
First-order reasoning and efficient semi-algebraic proofs.Fedor Part, Neil Thapen & Iddo Tzameret - 2025 - Annals of Pure and Applied Logic 176 (1):103496.details Download Export citation Bookmark
Upper and lower Ramsey bounds in bounded arithmetic.Kerry Ojakian - 2005 - Annals of Pure and Applied Logic 135 (1-3):135-150.details Pudlák shows that bounded arithmetic proves an upper bound on the Ramsey number Rr . We will strengthen this result by improving the bound. We also investigate lower bounds, obtaining a non-constructive lower bound for the special case of 2 colors , by formalizing a use of the probabilistic method. A constructive lower bound is worked out for the case when the monochromatic set size is fixed to 3 . The constructive lower bound is used to prove two “reversals”. To (...) Download Export citation Bookmark
On some $$\Sigma ^{B}_{0}$$-formulae generalizing counting principles over $$V^{0}$$.Eitetsu Ken - forthcoming - Archive for Mathematical Logic:1-42.details We formalize various counting principles and compare their strengths over $$V^{0}$$ V 0. In particular, we conjecture the following mutual independence between: a uniform version of modular counting principles and the pigeonhole principle for injections, a version of the oddtown theorem and modular counting principles of modulus p, where p is any natural number which is not a power of 2, and a version of Fisher’s inequality and modular counting principles. Then, we give sufficient conditions to prove them. We give (...) Download Export citation Bookmark

1