Document Open Access Logo

Proof Complexity Lower Bounds from Algebraic Circuit Complexity

Authors Michael A. Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson

PDF
Thumbnail PDF

File

LIPIcs.CCC.2016.32.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Michael A. Forbes
Amir Shpilka
Iddo Tzameret
Avi Wigderson

Cite As Get BibTex

Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof Complexity Lower Bounds from Algebraic Circuit Complexity. In 31st Conference on Computational Complexity (CCC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 50, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CCC.2016.32

Abstract

We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the boolean setting for subsystems of Extended Frege proofs whose lines are circuits from restricted boolean circuit classes. Essentially all of the subsystems considered in this paper can simulate the well-studied Nullstellensatz proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity).

Our main contributions are two general methods of converting certain algebraic lower bounds into proof complexity ones. Both require stronger arithmetic lower bounds than common, which should hold not for a specific polynomial but for a whole family defined by it. These may be likened to some of the methods by which Boolean circuit lower bounds are turned into related proof-complexity ones, especially the "feasible interpolation" technique. We establish algebraic lower bounds of these forms for several explicit polynomials, against a variety of classes, and infer the relevant proof complexity bounds. These yield separations between IPS subsystems, which we complement by simulations to create a partial structure theory for IPS systems.

Our first method is a functional lower bound, a notion of Grigoriev and Razborov, which is a function f' from n-bit strings to a field, such that any polynomial f agreeing with f' on the boolean cube requires large algebraic circuit complexity.  We develop functional lower bounds for a variety of circuit classes (sparse polynomials, depth-3 powering formulas, read-once algebraic branching programs and multilinear formulas) where f'(x) equals 1/p(x) for a constant-degree polynomial p depending on the relevant circuit class. We believe these lower bounds are of independent interest in algebraic complexity, and show that they also imply lower bounds for the size of the corresponding IPS refutations for proving that the relevant polynomial p is non-zero over the boolean cube. In particular, we show super-polynomial lower bounds for refuting variants of the subset-sum axioms in these IPS subsystems.

Our second method is to give lower bounds for multiples, that is, to give explicit polynomials whose all (non-zero) multiples require large algebraic circuit complexity. By extending known techniques, we give lower bounds for multiples for various restricted circuit classes such sparse polynomials, sums of powers of low-degree polynomials, and roABPs. These results are of independent interest, as we argue that lower bounds for multiples is the correct notion for instantiating the algebraic hardness versus randomness paradigm of Kabanets and Impagliazzo. Further, we show how such lower bounds for multiples extend to lower bounds for refutations in the corresponding IPS subsystem.

Subject Classification

Keywords
  • Proof Complexity
  • Algebraic Complexity
  • Nullstellensatz
  • Subset-Sum

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Manindra Agrawal. Proving lower bounds via pseudo-random generators. In Proceedings of the \nth\intcalcSub20051980 International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005), pages 92-105, 2005. URL: http://dx.doi.org/10.1007/11590156_6.
  2. Manindra Agrawal, Rohit Gurjar, Arpita Korwar, and Nitin Saxena. Hitting-sets for ROABP and sum of set-multilinear circuits. arXiv, 1406.7535, 2014. URL: http://arxiv.org/abs/1406.7535.
  3. Manindra Agrawal, Chandan Saha, and Nitin Saxena. Quasi-polynomial hitting-set for set-depth-Δ formulas. In Proceedings of the \nth\intcalcSub20131968 Annual ACM Symposium on Theory of Computing (STOC 2013), pages 321-330, 2013. Full version at http://arxiv.org/abs/1209.2333. URL: http://dx.doi.org/10.1145/2488608.2488649.
  4. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. In Proceedings of the \ifnumcomp2001<1966\nth\intcalcSub20011959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 2001)\ifnumcomp2001<1975\nth\intcalcSub20011959 Annual Symposium on Switching and Automata Theory (SWAT 2001)\nth\intcalcSub20011959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 2001), pages 190-199, 2001. URL: http://dx.doi.org/10.1109/SFCS.2001.959893.
  5. Matthew Anderson, Michael A. Forbes, Ramprasad Saptharishi, Amir Shpilka, and Ben Lee Volk. Identity testing and lower bounds for read-k oblivious algebraic branching programs. Electronic Colloquium on Computational Complexity (ECCC), 22:184, 2015. URL: http://eccc.hpi-web.de/report/2015/184/.
  6. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc. (3), 73(1):1-26, 1996. Preliminary version in the \ifnumcomp1994<1966\nth\intcalcSub19941959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 1994)\ifnumcomp1994<1975\nth\intcalcSub19941959 Annual Symposium on Switching and Automata Theory (SWAT 1994)\nth\intcalcSub19941959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 1994). URL: http://dx.doi.org/10.1112/plms/s3-73.1.1.
  7. Paul Beame and Toniann Pitassi. Propositional proof complexity: past, present, and future. Bull. Eur. Assoc. Theor. Comput. Sci. EATCS, 1998(65):66-89, 1998. Google Scholar
  8. Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. Syst. Sci., 62(2):267-289, 2001. Preliminary version in the \ifnumcomp1999<1996\nth\intcalcSub19991985 Annual Structure in Complexity Theory Conference (Structures 1999)\ifnumcomp1999<2015\nth\intcalcSub19991985 Annual IEEE Conference on Computational Complexity (CCC 1999)\nth\intcalcSub19991985 Annual Computational Complexity Conference (CCC 1999). URL: http://dx.doi.org/10.1006/jcss.2000.1726.
  9. Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity, 6(3):256-298, 1996. URL: http://dx.doi.org/10.1007/BF01294258.
  10. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the \nth\intcalcSub19961968 Annual ACM Symposium on Theory of Computing (STOC 1996), pages 174-183, 1996. URL: http://dx.doi.org/10.1145/237814.237860.
  11. Stephen A. Cook and Robert A. Reckhow. aOn the lengths of proofs in the propositional calculus (preliminary version). In Proceedings of the \nth\intcalcSub19741968 Annual ACM Symposium on Theory of Computing (STOC 1974), pages 135-148, 1974. For corrections see Cook-Reckhow [12]. URL: http://dx.doi.org/10.1145/800119.803893.
  12. Stephen A. Cook and Robert A. Reckhow. bCorrections for "On the lengths of proofs in the propositional calculus (preliminary version)". SIGACT News, 6(3):15-22, July 1974. URL: http://dx.doi.org/10.1145/1008311.1008313.
  13. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. This is a journal-version of Cook-Reckhow \citeCookReckhow74a and Reckhow [51]. URL: http://dx.doi.org/10.2307/2273702.
  14. Zeev Dvir, Amir Shpilka, and Amir Yehudayoff. Hardness-randomness tradeoffs for bounded depth arithmetic circuits. SIAM J. Comput., 39(4):1279-1293, 2009. Preliminary version in the \nth\intcalcSub20081968 Annual ACM Symposium on Theory of Computing (STOC 2008). URL: http://dx.doi.org/10.1137/080735850.
  15. Ismor Fischer. Sums of like powers of multivariate linear forms. Mathematics Magazine, 67(1):59-61, 1994. URL: http://www.jstor.org/stable/2690560.
  16. Michael A. Forbes. Polynomial Identity Testing of Read-Once Oblivious Algebraic Branching Programs. PhD thesis, Massachusetts Institute of Technology, June 2014. URL: http://hdl.handle.net/1721.1/89843.
  17. Michael A. Forbes. Deterministic divisibility testing via shifted partial derivatives. In Proceedings of the \ifnumcomp2015<1966\nth\intcalcSub20151959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 2015)\ifnumcomp2015<1975\nth\intcalcSub20151959 Annual Symposium on Switching and Automata Theory (SWAT 2015)\nth\intcalcSub20151959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 2015), 2015. Google Scholar
  18. Michael A. Forbes, Mrinal Kumar, and Ramprasad Saptharishi. Functional lower bounds for arithmetic circuits and boolean circuit complexity. Manuscript, 2015. Google Scholar
  19. Michael A. Forbes, Ramprasad Saptharishi, and Amir Shpilka. Hitting sets for multilinear read-once algebraic branching programs, in any order. In Proceedings of the \nth\intcalcSub20141968 Annual ACM Symposium on Theory of Computing (STOC 2014), pages 867-875, 2014. Full version at http://arxiv.org/abs/1309.5668. URL: http://dx.doi.org/10.1145/2591796.2591816.
  20. Michael A. Forbes and Amir Shpilka. On identity testing of tensors, low-rank recovery and compressed sensing. In Proceedings of the \nth\intcalcSub20121968 Annual ACM Symposium on Theory of Computing (STOC 2012), pages 163-172, 2012. Full version at http://arxiv.org/abs/1111.0663. URL: http://dx.doi.org/10.1145/2213977.2213995.
  21. Michael A. Forbes and Amir Shpilka. Explicit Noether Normalization for simultaneous conjugation via polynomial identity testing. In Proceedings of the \nth\intcalcSub20131996 International Workshop on Randomization and Computation (RANDOM 2013), pages 527-542, 2013. Full version at http://arxiv.org/abs/1303.0084. URL: http://dx.doi.org/10.1007/978-3-642-40328-6_37.
  22. Michael A. Forbes and Amir Shpilka. Quasipolynomial-time identity testing of non-commutative and read-once oblivious algebraic branching programs. In Proceedings of the \ifnumcomp2013<1966\nth\intcalcSub20131959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 2013)\ifnumcomp2013<1975\nth\intcalcSub20131959 Annual Symposium on Switching and Automata Theory (SWAT 2013)\nth\intcalcSub20131959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 2013), pages 243-252, 2013. Full version at http://arxiv.org/abs/1209.2408. URL: http://dx.doi.org/10.1109/FOCS.2013.34.
  23. Dima Grigoriev. Tseitin’s tautologies and lower bounds for Nullstellensatz proofs. In Proceedings of the \ifnumcomp1998<1966\nth\intcalcSub19981959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 1998)\ifnumcomp1998<1975\nth\intcalcSub19981959 Annual Symposium on Switching and Automata Theory (SWAT 1998)\nth\intcalcSub19981959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 1998), pages 648-652, 1998. URL: http://dx.doi.org/10.1109/SFCS.1998.743515.
  24. Dima Grigoriev and Marek Karpinski. An exponential lower bound for depth 3 arithmetic circuits. In Proceedings of the \nth\intcalcSub19981968 Annual ACM Symposium on Theory of Computing (STOC 1998), pages 577-582, 1998. URL: http://dx.doi.org/10.1145/276698.276872.
  25. Dima Grigoriev and Alexander A. Razborov. Exponential lower bounds for depth 3 arithmetic circuits in algebras of functions over finite fields. Appl. Algebra Eng. Commun. Comput., 10(6):465-487, 2000. Preliminary version in the \ifnumcomp1998<1966\nth\intcalcSub19981959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 1998)\ifnumcomp1998<1975\nth\intcalcSub19981959 Annual Symposium on Switching and Automata Theory (SWAT 1998)\nth\intcalcSub19981959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 1998). URL: http://dx.doi.org/10.1007/s002009900021.
  26. Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing. In Proceedings of the \ifnumcomp2014<1966\nth\intcalcSub20141959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 2014)\ifnumcomp2014<1975\nth\intcalcSub20141959 Annual Symposium on Switching and Automata Theory (SWAT 2014)\nth\intcalcSub20141959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 2014), pages 110-119, 2014. Full version at http://arxiv.org/abs/abs/1404.3820. URL: http://dx.doi.org/10.1109/FOCS.2014.20.
  27. Ankit Gupta, Pritish Kamath, Neeraj Kayal, and Ramprasad Saptharishi. Approaching the chasm at depth four. J. ACM, 61(6):33:1-33:16, December 2014. Preliminary version in the \ifnumcomp2013<1996\nth\intcalcSub20131985 Annual Structure in Complexity Theory Conference (Structures 2013)\ifnumcomp2013<2015\nth\intcalcSub20131985 Annual IEEE Conference on Computational Complexity (CCC 2013)\nth\intcalcSub20131985 Annual Computational Complexity Conference (CCC 2013). URL: http://dx.doi.org/10.1145/2629541.
  28. Joos Heintz and Claus-Peter Schnorr. Testing polynomials which are easy to compute (extended abstract). In Proceedings of the \nth\intcalcSub19801968 Annual ACM Symposium on Theory of Computing (STOC 1980), pages 262-272, 1980. URL: http://dx.doi.org/10.1145/800141.804674.
  29. Pavel Hrubes and Iddo Tzameret. Short proofs for the determinant identities. SIAM J. Comput., 44(2):340-383, 2015. Preliminary version in the \nth\intcalcSub20121968 Annual ACM Symposium on Theory of Computing (STOC 2012). URL: http://dx.doi.org/10.1137/130917788.
  30. Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall. Lower bounds for the polynomial calculus and the gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. URL: http://dx.doi.org/10.1007/s000370050024.
  31. Valentine Kabanets and Russell Impagliazzo. Derandomizing polynomial identity tests means proving circuit lower bounds. Computational Complexity, 13(1-2):1-46, 2004. Preliminary version in the \nth\intcalcSub20031968 Annual ACM Symposium on Theory of Computing (STOC 2003). URL: http://dx.doi.org/10.1007/s00037-004-0182-6.
  32. Erich L. Kaltofen. Factorization of polynomials given by straight-line programs. In Silvio Micali, editor, Randomness and Computation, volume 5 of Advances in Computing Research, pages 375-412. JAI Press, Inc., Greenwich, CT, USA, 1989. URL: http://www.math.ncsu.edu/~kaltofen/bibliography/89/Ka89_slpfac.pdf.
  33. Neeraj Kayal. Personal Communication to Saxena [52], 2008. Google Scholar
  34. Neeraj Kayal. An exponential lower bound for the sum of powers of bounded degree polynomials. Electronic Colloquium on Computational Complexity (ECCC), 19(81), 2012. URL: http://eccc.hpi-web.de/report/2012/081.
  35. Jan Krajíček. Bounded arithmetic, propositional logic, and complexity theory, volume 60 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1995. URL: http://dx.doi.org/10.1017/CBO9780511529948.
  36. Mrinal Kumar and Ramprasad Saptharishi. An exponential lower bound for homogeneous depth-5 circuits over finite fields. arXiv, 1507.00177, 2015. URL: http://arxiv.org/abs/1507.00177.
  37. Fu Li, Iddo Tzameret, and Zhengyu Wang. Non-commutative formulas and Frege lower bounds: a new characterization of propositional proofs. In Proceedings of the 30th Computational Complexity Conference (CCC), June 17-19, 2015, 2015. Google Scholar
  38. Noam Nisan. Lower bounds for non-commutative computation. In Proceedings of the \nth\intcalcSub19911968 Annual ACM Symposium on Theory of Computing (STOC 1991), pages 410-418, 1991. URL: http://dx.doi.org/10.1145/103418.103462.
  39. Noam Nisan and Avi Wigderson. Hardness vs randomness. J. Comput. Syst. Sci., 49(2):149-167, 1994. Preliminary version in the \ifnumcomp1988<1966\nth\intcalcSub19881959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 1988)\ifnumcomp1988<1975\nth\intcalcSub19881959 Annual Symposium on Switching and Automata Theory (SWAT 1988)\nth\intcalcSub19881959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 1988). URL: http://dx.doi.org/10.1016/S0022-0000(05)80043-1.
  40. Noam Nisan and Avi Wigderson. Lower bounds on arithmetic circuits via partial derivatives. Computational Complexity, 6(3):217-234, 1996. Preliminary version in the \ifnumcomp1995<1966\nth\intcalcSub19951959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 1995)\ifnumcomp1995<1975\nth\intcalcSub19951959 Annual Symposium on Switching and Automata Theory (SWAT 1995)\nth\intcalcSub19951959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 1995). URL: http://dx.doi.org/10.1007/BF01294256.
  41. Rafael Oliveira. Factors of low individual degree polynomials. In Proceedings of the \ifnumcomp2015<1996\nth\intcalcSub20151985 Annual Structure in Complexity Theory Conference (Structures 2015)\ifnumcomp2015<2015\nth\intcalcSub20151985 Annual IEEE Conference on Computational Complexity (CCC 2015)\nth\intcalcSub20151985 Annual Computational Complexity Conference (CCC 2015), volume 33 of Leibniz International Proceedings in Informatics (LIPIcs), pages 198-216, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CCC.2015.198.
  42. Rafael Oliveira, Amir Shpilka, and Ben Lee Volk. Subexponential size hitting sets for bounded depth multilinear formulas. In Proceedings of the \ifnumcomp2015<1996\nth\intcalcSub20151985 Annual Structure in Complexity Theory Conference (Structures 2015)\ifnumcomp2015<2015\nth\intcalcSub20151985 Annual IEEE Conference on Computational Complexity (CCC 2015)\nth\intcalcSub20151985 Annual Computational Complexity Conference (CCC 2015), volume 33 of Leibniz International Proceedings in Informatics (LIPIcs), pages 304-322, 2015. Full version at http://arxiv.org/abs/1411.7492. URL: http://dx.doi.org/10.4230/LIPIcs.CCC.2015.304.
  43. Toniann Pitassi. Algebraic propositional proof systems. In Descriptive complexity and finite models (Princeton, NJ, 1996), volume 31 of DIMACS Ser. Discrete Math. Theoret. Comput. Sci., pages 215-244. Amer. Math. Soc., Providence, RI, 1997. Google Scholar
  44. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, Sept. 1997. Google Scholar
  45. Ran Raz. Separation of multilinear circuit and formula size. Theory of Computing, 2(6):121-135, 2006. Preliminary version in the \ifnumcomp2004<1966\nth\intcalcSub20041959 Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 2004)\ifnumcomp2004<1975\nth\intcalcSub20041959 Annual Symposium on Switching and Automata Theory (SWAT 2004)\nth\intcalcSub20041959 Annual IEEE Symposium on Foundations of Computer Science (FOCS 2004). URL: http://dx.doi.org/10.4086/toc.2006.v002a006.
  46. Ran Raz. Multi-linear formulas for permanent and determinant are of super-polynomial size. J. ACM, 56(2), 2009. Preliminary version in the \nth\intcalcSub20041968 Annual ACM Symposium on Theory of Computing (STOC 2004). URL: http://dx.doi.org/10.1145/1502793.1502797.
  47. Ran Raz and Amir Shpilka. Deterministic polynomial identity testing in non-commutative models. Comput. Complex., 14(1):1-19, April 2005. Preliminary version in the \ifnumcomp2004<1996\nth\intcalcSub20041985 Annual Structure in Complexity Theory Conference (Structures 2004)\ifnumcomp2004<2015\nth\intcalcSub20041985 Annual IEEE Conference on Computational Complexity (CCC 2004)\nth\intcalcSub20041985 Annual Computational Complexity Conference (CCC 2004). URL: http://dx.doi.org/10.1007/s00037-005-0188-8.
  48. Ran Raz and Iddo Tzameret. The strength of multilinear proofs. Computational Complexity, 17(3):407-457, 2008. Google Scholar
  49. Ran Raz and Amir Yehudayoff. Lower bounds and separations for constant depth multilinear circuits. Computational Complexity, 18(2):171-207, 2009. Preliminary version in the \ifnumcomp2008<1996\nth\intcalcSub20081985 Annual Structure in Complexity Theory Conference (Structures 2008)\ifnumcomp2008<2015\nth\intcalcSub20081985 Annual IEEE Conference on Computational Complexity (CCC 2008)\nth\intcalcSub20081985 Annual Computational Complexity Conference (CCC 2008). URL: http://dx.doi.org/10.1007/s00037-009-0270-8.
  50. Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, 1998. URL: http://dx.doi.org/10.1007/s000370050013.
  51. Robert A. Reckhow. On the lengths of proofs in the propositional calculus. PhD thesis, University of Toronto, 1976. URL: https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf.
  52. Nitin Saxena. Diagonal circuit identity testing and lower bounds. In Proceedings of the \nth\intcalcSub20081973 International Colloquium on Automata, Languages and Programming (ICALP 2008), pages 60-71, 2008. Preliminary version in the \ECCCurl07124. URL: http://dx.doi.org/10.1007/978-3-540-70575-8_6.
  53. Amir Shpilka. Affine projections of symmetric polynomials. J. Comput. Syst. Sci., 65(4):639-659, 2002. Preliminary version in the \ifnumcomp2001<1996\nth\intcalcSub20011985 Annual Structure in Complexity Theory Conference (Structures 2001)\ifnumcomp2001<2015\nth\intcalcSub20011985 Annual IEEE Conference on Computational Complexity (CCC 2001)\nth\intcalcSub20011985 Annual Computational Complexity Conference (CCC 2001). URL: http://dx.doi.org/10.1016/S0022-0000(02)00021-1.
  54. Amir Shpilka and Amir Yehudayoff. Arithmetic circuits: A survey of recent results and open questions. Foundations and Trends in Theoretical Computer Science, 5(3-4):207-388, 2010. URL: http://dx.doi.org/10.1561/0400000039.
  55. Michael Soltys and Stephen Cook. The proof complexity of linear algebra. Ann. Pure Appl. Logic, 130(1-3):277-323, 2004. Google Scholar
  56. Iddo Tzameret. Algebraic proofs over noncommutative formulas. Information and Computation, 209(10):1269-1292, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact