Uniform, integral and efficient proofs for the determinant identities

Iddo Tzameret, Stephen Cook

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

60 Downloads (Pure)


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


  • Bounded Arithmetic, Computational Complexity, proof complexity

Cite this