Uniform, integral and efficient proofs for the determinant identities. / Tzameret, Iddo; Cook, Stephen.

2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Vol. 32 IEEE, 2017. p. 1-12.

Research output: Chapter in Book/Report/Conference proceedingConference contribution




We 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 provable in the bounded arithmetic theory VNC2, which is a first-order theory corresponding to the complexity class NC2. This also establishes the existence of uniform polynomial-size and O(log2n)-depth Circuit-Frege (equivalently, Extended Frege) proofs over the integers, of the basic determinant identities (previous proofs hold only over GF(2)). In doing so, we give uniform NC2-algorithms for homogenizing algebraic circuits, balancing algebraic circuits (given as input an upper bound on the syntactic-degree of the circuit), and converting circuits with divisions into circuits with a single division gate—all (Σ1B-) definable in VNC2. This also implies an NC2-algorithm for evaluating algebraic circuits of any depth.
Original languageEnglish
Title of host publication 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Number of pages12
ISBN (Electronic)978-1-5090-3018-7
ISBN (Print)978-1-5090-3019-4
Publication statusPublished - 18 Aug 2017
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 28116759