{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T13:15:52Z","timestamp":1648646152814},"reference-count":21,"publisher":"World Scientific Pub Co Pte Lt","issue":"02","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Algebra Comput."],"published-print":{"date-parts":[[2018,3]]},"abstract":"<jats:p>We use results from the theory of algebras with polynomial identities (PI-algebras) to study the witness complexity of matrix identities. A matrix identity of [Formula: see text] matrices over a field [Formula: see text]is a non-commutative polynomial (f(x<jats:sub>1<\/jats:sub>, \u2026, x<jats:sub>n<\/jats:sub>)) over [Formula: see text], such that [Formula: see text] vanishes on every [Formula: see text] matrix assignment to its variables. For every field [Formula: see text]of characteristic 0, every [Formula: see text] and every finite basis of [Formula: see text] matrix identities over [Formula: see text], we show there exists a family of matrix identities [Formula: see text], such that each [Formula: see text] has [Formula: see text] variables and requires at least [Formula: see text] many generators to generate, where the generators are substitution instances of elements from the basis. The lower bound argument uses fundamental results from PI-algebras together with a generalization of the arguments in [P. Hrube\u0161, How much commutativity is needed to prove polynomial identities? Electronic colloquium on computational complexity, ECCC, Report No.: TR11-088, June 2011].<\/jats:p><jats:p>We apply this result in algebraic proof complexity, focusing on proof systems for polynomial identities (PI proofs) which operate with algebraic circuits and whose axioms are the polynomial-ring axioms [P. Hrube\u0161 and I. Tzameret, The proof complexity of polynomial identities, in Proc. 24th Annual IEEE Conf. Computational Complexity, CCC 2009, 15\u201318 July 2009, Paris, France (2009), pp. 41\u201351; Short proofs for the determinant identities, SIAM J. Comput. 44(2) (2015) 340\u2013383], and their subsystems. We identify a decrease in strength hierarchy of subsystems of PI proofs, in which the [Formula: see text]th level is a sound and complete proof system for proving [Formula: see text] matrix identities (over a given field). For each level [Formula: see text] in the hierarchy, we establish an [Formula: see text] lower bound on the number of proof-steps needed to prove certain identities.<\/jats:p><jats:p>Finally, we present several concrete open problems about non-commutative algebraic circuits and speed-ups in proof complexity, whose solution would establish stronger size lower bounds on PI proofs of matrix identities, and beyond.<\/jats:p>","DOI":"10.1142\/s021819671850011x","type":"journal-article","created":{"date-parts":[[2018,1,25]],"date-time":"2018-01-25T10:31:03Z","timestamp":1516876263000},"page":"217-256","source":"Crossref","is-referenced-by-count":1,"title":["Witnessing matrix identities and proof complexity"],"prefix":"10.1142","volume":"28","author":[{"given":"Fu","family":"Li","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Texas at Austin, Austin, Texas, TX 78712, USA"}]},{"given":"Iddo","family":"Tzameret","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Royal Holloway, University of London, Egham Hill, Egham, TW20 0EX, UK"}]}],"member":"219","published-online":{"date-parts":[[2018,3,27]]},"reference":[{"key":"S021819671850011XBIB001","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2015.12.008"},{"key":"S021819671850011XBIB002","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1950-0036751-9"},{"key":"S021819671850011XBIB004","doi-asserted-by":"publisher","DOI":"10.1201\/9780203911549.ch5"},{"key":"S021819671850011XBIB005","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539705447359"},{"key":"S021819671850011XBIB006","doi-asserted-by":"publisher","DOI":"10.1145\/1008311.1008313"},{"key":"S021819671850011XBIB008","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"issue":"3","key":"S021819671850011XBIB009","first-page":"291","volume":"20","author":"Drensky V.","year":"1981","journal-title":"Algebra i Logika"},{"key":"S021819671850011XBIB010","volume-title":"Free Algebras and PI-Algebras","author":"Drensky V.","year":"1999"},{"key":"S021819671850011XBIB012","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","volume":"185","author":"Biere A.","year":"2009"},{"key":"S021819671850011XBIB015","doi-asserted-by":"publisher","DOI":"10.1137\/130917788"},{"key":"S021819671850011XBIB016","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2011.v007a008"},{"key":"S021819671850011XBIB017","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.12.003"},{"key":"S021819671850011XBIB019","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-004-0182-6"},{"key":"S021819671850011XBIB020","doi-asserted-by":"publisher","DOI":"10.1007\/BF01978692"},{"key":"S021819671850011XBIB021","volume-title":"Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encyclopedia of Mathematics and its Applications","volume":"60","author":"Kraj\u00ed\u010dek J.","year":"1995"},{"key":"S021819671850011XBIB022","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1973-0332873-3"},{"issue":"3","key":"S021819671850011XBIB024","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/2984450.2984455","volume":"3","author":"Pitassi T.","year":"2016","journal-title":"ACM SIGLOG News"},{"key":"S021819671850011XBIB025","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-005-0188-8"},{"key":"S021819671850011XBIB027","series-title":"Pure and Applied Mathematics","volume-title":"Polynomial Identities in Ring Theory","author":"Rowen L. H.","year":"1980"},{"key":"S021819671850011XBIB028","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322225"},{"key":"S021819671850011XBIB029","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.07.004"}],"container-title":["International Journal of Algebra and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S021819671850011X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T03:01:19Z","timestamp":1603681279000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S021819671850011X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3]]},"references-count":21,"journal-issue":{"issue":"02","published-online":{"date-parts":[[2018,3,27]]},"published-print":{"date-parts":[[2018,3]]}},"alternative-id":["10.1142\/S021819671850011X"],"URL":"https:\/\/doi.org\/10.1142\/s021819671850011x","relation":{},"ISSN":["0218-1967","1793-6500"],"issn-type":[{"value":"0218-1967","type":"print"},{"value":"1793-6500","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3]]}}}