We give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF(2) in Hrubeš-Tzameret . 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.
|Title of host publication||2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)|
|Number of pages||12|
|Publication status||Published - 18 Aug 2017|
- Bounded Arithmetic, Computational Complexity, proof complexity