Short Proofs for the Determinant Identities

Details Short Proofs for the Determinant Identities Short Proofs for the Determinant Identities

2011-12-29

arxiv.org/abs/1112.6265v1

Computer Science

Computational Complexity

41 pages

Scientific paper

We study arithmetic proof systems P_c(F) and P_f(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 one stating that P_c(F) proofs can be balanced: if a polynomial identity of syntactic degree d and depth k has a P_c(F) proof of size s, then it also has a P_c(F) proof of size poly(s,d) and depth O(k+\log^2 d + \log d\cd \log s). As a corollary, we obtain a quasipolynomial simulation of P_c(F) by P_f(F), for identities of a polynomial syntactic degree. Using these results we obtain the following: consider the identities det(XY) = det(X)det(Y) and det(Z)= z_{11}... z_{nn}, where X,Y and Z are nxn square matrices and Z is a triangular matrix with z_{11},..., z_{nn} on the diagonal (and det is the determinant polynomial). Then we can construct a polynomial-size arithmetic circuit det such that the above identities have P_c(F) proofs of polynomial-size and O(\log^2 n) depth. Moreover, there exists an arithmetic formula det of size n^{O(\log n)} such that the above identities have P_f(F) proofs of size n^{O(\log n)}. This yields a solution to a long-standing open problem in propositional proof complexity, namely, whether there are polynomial-size NC^2-Frege proofs for the determinant identities and the hard matrix identities, as considered, e.g., in Soltys and Cook (2004) (cf., Beame and Pitassi (1998)). We show that matrix identities like AB=I {\to} BA=I (for matrices over the two element field) as well as basic properties of the determinant have polynomial-size NC^2-Frege proofs, and quasipolynomial-size Frege proofs.

Affiliated with

Also associated with

No associations

Rating

Short Proofs for the Determinant Identities does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Short Proofs for the Determinant Identities, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Short Proofs for the Determinant Identities will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-728406