Cited By
View all- Ken E(2024)On some $$\Sigma ^{B}_{0}$$-formulae generalizing counting principles over $$V^{0}$$Archive for Mathematical Logic10.1007/s00153-024-00938-1Online publication date: 22-Jul-2024
Uniform, Integral, and Feasible Proofs for the Determinant Identities
Article No.: 12, Pages 1 - 80
Abstract
Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF(2) in Hrubeš-Tzameret [15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory VNC2; the latter is a first-order theory corresponding to the complexity class NC2 consisting of problems solvable by uniform families of polynomial-size circuits and O(log2 n)-depth. This also establishes the existence of uniform polynomial-size propositional proofs operating with NC2-circuits of the basic determinant identities over the integers (previous propositional proofs hold only over the two-element field).
References
[1]
Eric Allender. 2018. Personal com
[2]
Eric Allender, Jia Jiao, Meena Mahajan, and V. Vinay. 1998. Non-commutative arithmetic circuits: Depth reduction and size lower bounds. Theor. Comput. Sci. 209, 1--2 (1998), 47--86.
[3]
Paul Beame and Toniann Pitassi. 1998. Propositional proof complexity: Past, present, and future. Bull. Eur. Assoc. Theor. Comput. Sci. 65 (1998), 66--89.
[4]
Stuart J. Berkowitz. 1984. On computing the determinant in small parallel time using a small number of processors. Inf. Proc. Lett. 18 (1984), 147--150.
[5]
Maria Luisa Bonet, Samuel R. Buss, and Toniann Pitassi. 1995. Are there hard examples for Frege systems? In Feasible Mathematics, II(Progress in Computer Science and Applied Logic, Vol. 13). Birkhäuser Boston, Boston, MA, 30--56.
[6]
Sam Buss, Valentine Kabanets, Antonina Kolokolova, and Michal Koucky. 2017. Expander construction in VNC. Ann. Pure. Appl. Logic 171, 7 (2020), 102796.
[7]
Samuel R. Buss. 1986. Bounded Arithmetic (Studies in Proof Theory, Vol. 3). Bibliopolis.
[8]
Samuel R. Buss, Leszek Aleksander Kolodziejczyk, and Konrad Zdanowski. 2015. Collapsing modular counting in bounded arithmetic and constant depth propositional proofs. Trans. Amer. Math. Soc. 367 (2015), 7517--7563.
[9]
Stephen Cook and Phuong Nguyen. 2010. Logical Foundations of Proof Complexity. ASL Perspectives in Logic. Cambridge University Press.
[10]
Stephen A. Cook. 1975. Feasibly constructive proofs and the propositional calculus (preliminary version). In Proceedings of the ACM Symposium on Theory of Computing (STOC’75). 83--97.
[11]
Stephen A. Cook. 1985. A taxonomy of problems with fast parallel algorithms. Inf. Contr. 64, 1--3 (1985), 2--21.
[12]
Stephen A. Cook and Lila A. Fontes. 2012. Formal theories for linear algebra. Log. Meth. Comput. Sci. 8, 1 (2012).
[13]
P. Hájek and P. Pudlák. 1993. Metamathematics of First-order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin.
[14]
Pavel Hrubeš and Iddo Tzameret. 2009. The proof complexity of polynomial identities. In Proceedings of the 24th IEEE Conference on Computational Complexity (CCC’09). 41--51.
[15]
Pavel Hrubeš and Iddo Tzameret. 2015. Short proofs for the determinant identities. SIAM J. Comput. 44, 2 (2015), 340--383.
[16]
Emil Jeřábek. 2004. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Ann. Pure Appl. Log. 129, 1-3 (2004), 1--37.
[17]
Emil Jeřábek. 2005. Weak Pigeonhole Principle, and Randomized Computation. PhD thesis. Faculty of Mathematics and Physics, Charles University, Prague.
[18]
Emil Jeřábek. 2011. A sorting network in bounded arithmetic. Ann. Pure Appl. Log. 162, 4 (2011), 341--355.
[19]
Jan Krajíček. 1995. Bounded Arithmetic, Propositional Logic, and Complexity Theory(Encyclopedia of Mathematics and its Applications, Vol. 60). Cambridge University Press, Cambridge.
[20]
Gary L. Miller, Vijaya Ramachandran, and Erich Kaltofen. 1988. Efficient parallel evaluation of straight-line code and arithmetic circuits. SIAM J. Comput. 17, 4 (1988), 687--695.
[21]
Sebastian Müller and Iddo Tzameret. 2014. Short propositional refutations for dense random 3CNF formulas. Ann. Pure Appl. Log. 165 (2014), 1864--1918.
[22]
Phuong Nguyen. 2008. Bounded Reverse Mathematics. PhD thesis. University of Toronto.
[23]
Phuong Nguyen and Stephen Cook. 2007. The complexity of proving discrete Jordan curve theorem. In Proceedings of the 22nd IEEE Symposium on Logic in Computer. 245--254.
[24]
Rohit Parikh. 1971. Existence and feasibility in arithmetic. J. Symbol. Log. 36 (1971), 494--508.
[25]
J. Paris and A. Wilkie. 1985. Counting problems in bounded arithmetic. In Methods in Mathematical Logic (Caracas, 1983)(Lecture Notes in Mathematics, Vol. 1130). Springer, Berlin, 317--340.
[26]
Ján Pich. 2015. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic. Log. Meth. Comput. Sci. 11, 2 (2015).
[27]
Tonnian Pitassi and Iddo Tzameret. 2016. Algebraic proof complexity: Progress, frontiers and challenges. ACM SIGLOG News 3, 3 (2016).
[28]
Ran Raz and Amir Yehudayoff. 2008. Balancing syntactically multilinear arithmetic circuits. Comput. Complex. 17, 4 (2008), 515--535.
[29]
J. T. Schwartz. 1980. Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27, 4 (1980), 701--717.
[30]
Amir Shpilka and Amir Yehudayoff. 2010. Arithmetic circuits: A survey of recent results and open questions. Found. Trends Theor. Comput. Sci. 5, 3--4 (2010), 207--388.
[31]
Stephen Simpson. 1999. Subsystems of Second Order Arithmetic. Springer.
[32]
Michael Soltys. 2001. The Complexity of Derivations of Matrix Identities. PhD thesis. University of Toronto, Toronto, Canada.
[33]
Michael Soltys and Stephen Cook. 2004. The proof complexity of linear algebra. Ann. Pure Appl. Logic 130, 1--3 (2004), 277--323.
[34]
Volker Strassen. 1973. Vermeidung von divisionen. J. Reine Angew. Math. 264 (1973), 182--202. (in German).
[35]
Neil Thapen and Michael Soltys. 2005. Weak theories of linear algebra. Arch. Math. Log. 44, 2 (2005), 195--208.
[36]
Leslie G. Valiant, Sven Skyum, S. Berkowitz, and Charles Rackoff. 1983. Fast parallel computation of polynomials using few processors. SIAM J. Comput. 12, 4 (1983), 641--644.
[37]
V. Vinay. 1991. Counting auxiliary pushdown automata and semi-unbounded arithmetic circuits. In Proceedings of the 6th IEEE Structure in Complexity Theory Conference. 270--284.
[38]
Richard Zippel. 1979. Probabilistic algorithms for sparse polynomials. In Proceedings of the International Symposium on Symbolic and Algebraic Computation. Springer-Verlag, 216--226.
Index Terms
- Uniform, Integral, and Feasible Proofs for the Determinant Identities
Recommendations
Feasible Operations on Proofs: The Logic of Proofs for Bounded Arithmetic
This paper presents a semantics for the logic of proofs $\mathsf{LP}$ in which all the operations on proofs are realized by feasibly computable functions. More precisely, we will show that the completeness of $\mathsf{LP}$ for the semantics of proofs of ...
Short proofs for the determinant identities
STOC '12: Proceedings of the forty-fourth annual ACM symposium on Theory of computingWe study arithmetic proof systems Pc(F) and Pf(F) operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field F. We establish a series of structural theorems about these proof systems, the main ...
Uniform, integral and efficient proofs for the determinant identities
LICS '17: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer ScienceWe give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF(2) in Hrubeš-Tzameret [9]. Specifically, we show that the multiplicativity of the determinant function over the integers is ...
Comments
Information & Contributors
Information
Published In
April 2021
226 pages
Copyright © 2021 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 13 January 2021
Accepted: 01 October 2020
Revised: 01 October 2020
Received: 01 November 2018
Published in JACM Volume 68, Issue 2
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed
Funding Sources
- National Natural Science Foundation of China
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 173Total Downloads
- Downloads (Last 12 months)7
- Downloads (Last 6 weeks)0
Reflects downloads up to 07 Sep 2024
Other Metrics
Citations
Cited By
View all- Ken E(2024)On some $$\Sigma ^{B}_{0}$$-formulae generalizing counting principles over $$V^{0}$$Archive for Mathematical Logic10.1007/s00153-024-00938-1Online publication date: 22-Jul-2024
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML Format