{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T17:13:32Z","timestamp":1783617212981,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,7,12]],"date-time":"2026-07-12T00:00:00Z","timestamp":1783814400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Austrian Science Fund (FWF)","award":["10.55776\/COE12"],"award-info":[{"award-number":["10.55776\/COE12"]}]},{"name":"State of Upper Austria","award":["LIT AI Lab"],"award-info":[{"award-number":["LIT AI Lab"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,7,13]]},"DOI":"10.1145\/3815436.3815447","type":"proceedings-article","created":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T16:11:51Z","timestamp":1783613511000},"page":"209-218","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Refuting Noncommutative Ideal Membership via Matrix Certificates"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3025-0604","authenticated-orcid":false,"given":"Clemens","family":"Hofstadler","sequence":"first","affiliation":[{"name":"Johannes Kepler University Linz, Linz, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3680-4355","authenticated-orcid":false,"given":"Peter","family":"Krug","sequence":"additional","affiliation":[{"name":"University of Kassel, Kassel, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7735-3726","authenticated-orcid":false,"given":"Georg","family":"Regensburger","sequence":"additional","affiliation":[{"name":"Johannes Kepler University Linz, Linz, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,12]]},"reference":[{"key":"e_1_3_3_2_2_2","doi-asserted-by":"crossref","unstructured":"Shimshon\u00a0A. Amitsur. 1957. A Generalization of Hilbert\u2019s Nullstellensatz. Proc. Am. Math. Soc. 8 (1957) 649\u2013656.","DOI":"10.1090\/S0002-9939-1957-0087644-9"},{"key":"e_1_3_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-41724-5_3"},{"key":"e_1_3_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3452143.3465545"},{"key":"e_1_3_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"e_1_3_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373207.3404047"},{"key":"e_1_3_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Donald\u00a0J. Collins. 1986. A simple presentation of a group with unsolvable word problem. Ill. J. Math. 30 2 (1986) 230\u2013234.","DOI":"10.1215\/ijm\/1256044631"},{"key":"e_1_3_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77272-9_10"},{"key":"e_1_3_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Dragana\u00a0S. Cvetkovi\u0107-Ili\u0107 Clemens Hofstadler Jamal Hossein\u00a0Poor Jovana Milo\u0161evi\u0107 Clemens\u00a0G. Raab and Georg Regensburger. 2021. Algebraic proof methods for identities of matrices and operators: improvements of Hartwig\u2019s triple reverse order law. Appl. Math. Comput. 409 (2021) 126357.","DOI":"10.1016\/j.amc.2021.126357"},{"key":"e_1_3_3_2_11_2","doi-asserted-by":"crossref","unstructured":"David Eisenbud and Melvin Hochster. 1979. A Nullstellensatz with Nilpotents and Zariski\u2019s Main Lemma on Holomorphic Functions. J. Algebra 58 (1979) 157\u2013161.","DOI":"10.1016\/0021-8693(79)90196-0"},{"key":"e_1_3_3_2_12_2","volume-title":"Modern Computer Algebra (3rd ed.)","author":"Gerhard J\u00fcrgen","year":"2013","unstructured":"J\u00fcrgen Gerhard and Joachim Von\u00a0zur Gathen. 2013. Modern Computer Algebra (3rd ed.). Cambridge University Press."},{"key":"e_1_3_3_2_13_2","doi-asserted-by":"crossref","unstructured":"Joshua\u00a0A. Grochow. 2025. Multivariate Hensel Lifting Without Assuming as Many Variables as Equations. Am. Math. Mon. 132 4 (2025) 350\u2013355.","DOI":"10.1080\/00029890.2024.2440297"},{"key":"e_1_3_3_2_14_2","doi-asserted-by":"crossref","unstructured":"Robert\u00a0E. Hartwig. 1986. The reverse order law revisited. Linear Algebra Appl. 76 (1986) 241\u2013246.","DOI":"10.1016\/0024-3795(86)90226-0"},{"key":"e_1_3_3_2_15_2","first-page":"79","volume-title":"Computer Algebra in Scientific Computing (CASC) 2025","author":"Heisinger Maximilian","year":"2025","unstructured":"Maximilian Heisinger and Clemens Hofstadler. 2025. f4ncgb: High Performance Gr\u00f6bner Basis Computations in Free Algebras. In Computer Algebra in Scientific Computing (CASC) 2025 , Vol.\u00a016235. 79\u201397."},{"key":"e_1_3_3_2_16_2","doi-asserted-by":"crossref","unstructured":"J.\u00a0William Helton Mark Stankus and John\u00a0J. Wavrik. 1998. Computer simplification of formulas in linear systems theory. IEEE Trans. Autom. Control 43 (1998) 302\u2013314.","DOI":"10.1109\/9.661584"},{"key":"e_1_3_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-8522-5_12"},{"key":"e_1_3_3_2_18_2","doi-asserted-by":"crossref","unstructured":"Marijn\u00a0JH Heule Manuel Kauers and Martina Seidl. 2021. New ways to multiply 3 \u00d7 3-matrices. J. Symb. Comput. 104 (2021) 899\u2013916.","DOI":"10.1016\/j.jsc.2020.10.003"},{"key":"e_1_3_3_2_19_2","unstructured":"Clemens Hofstadler. 2023. Noncommutative Gr\u00f6bner bases and automated proofs of operator statements. Ph.\u00a0D. Dissertation. Johannes Kepler University Linz Austria. Available at https:\/\/resolver.obvsg.at\/urn:nbn:at:at-ubl:1-67821."},{"key":"e_1_3_3_2_20_2","doi-asserted-by":"crossref","unstructured":"Clemens Hofstadler and Viktor Levandovskyy. 2026. Modular algorithms for computing Gr\u00f6bner bases in free algebras. J. Symb. Comput. 137 (2026) 102581.","DOI":"10.1016\/j.jsc.2026.102581"},{"key":"e_1_3_3_2_21_2","doi-asserted-by":"crossref","unstructured":"Clemens Hofstadler Clemens\u00a0G. Raab and Georg Regensburger. 2026. Universal truth of operator statements via ideal membership. J. Pure Appl. Algebra 230 4 (2026) 108221.","DOI":"10.1016\/j.jpaa.2026.108221"},{"key":"e_1_3_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597066.3597120"},{"key":"e_1_3_3_2_23_2","doi-asserted-by":"crossref","unstructured":"Igor Klep Victor Vinnikov and Jurij Vol\u010di\u010d. 2017. Null- and Positivstellens\u00e4tze for rationally resolvable ideals. Linear Algebra Appl. 527 (2017) 260\u2013293.","DOI":"10.1016\/j.laa.2017.04.009"},{"key":"e_1_3_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70628-1"},{"key":"e_1_3_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0041-0"},{"key":"e_1_3_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3476446.3535481"},{"key":"e_1_3_3_2_27_2","first-page":"305","volume-title":"Proceedings of ISSAC 2020","author":"Levandovskyy Viktor","year":"2020","unstructured":"Viktor Levandovskyy, Hans Sch\u00f6nemann, and Karim Abou\u00a0Zeid. 2020. Letterplace \u2013 a Subsystem of Singular for Computations with Free Algebras via Letterplace Embedding. In Proceedings of ISSAC 2020. 305\u2013311."},{"key":"e_1_3_3_2_28_2","unstructured":"Andrey\u00a0A. Markov. 1947. The impossibility of certain algorithms in the theory of associative systems I. Dokl. Akad. Nauk 55 (1947) 583\u2013586."},{"key":"e_1_3_3_2_29_2","doi-asserted-by":"crossref","unstructured":"Teo Mora. 1994. An introduction to commutative and noncommutative Gr\u00f6bner bases. Theor. Comput. Sci. 134 1 (1994) 131\u2013173.","DOI":"10.1016\/0304-3975(94)90283-6"},{"key":"e_1_3_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00233-021-10216-8"},{"key":"e_1_3_3_2_31_2","unstructured":"Carl-Fredrik Nyberg-Brodda. 2024. G.\u00a0S.\u00a0Tseytin\u2019s seven-relation semigroup with undecidable word problem. arxiv:https:\/\/arXiv.org\/abs\/2401.11757\u00a0[math.HO] https:\/\/arxiv.org\/abs\/2401.11757"},{"key":"e_1_3_3_2_32_2","doi-asserted-by":"crossref","unstructured":"Emil\u00a0L. Post. 1947. Recursive unsolvability of a problem of Thue. J. Symbolic. Logic 12 (1947) 1\u201311.","DOI":"10.2307\/2267170"},{"key":"e_1_3_3_2_33_2","doi-asserted-by":"crossref","unstructured":"Clemens\u00a0G. Raab Georg Regensburger and Jamal Hossein\u00a0Poor. 2021. Formal proofs of operator identities by a single formal computation. J. Pure Appl. Algebra 225 Article 106564 (2021).","DOI":"10.1016\/j.jpaa.2020.106564"},{"key":"e_1_3_3_2_34_2","doi-asserted-by":"crossref","unstructured":"Guy Salomon Orr\u00a0M. Shalit and Eli Shamovich. 2018. Algebras of bounded noncommutative analytic functions on subvarieties of the noncommutative unit ball. Trans. Amer. Math. Soc. 370 12 (2018) 8639\u20138690.","DOI":"10.1090\/tran\/7308"},{"key":"e_1_3_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_14"},{"key":"e_1_3_3_2_36_2","volume-title":"Blog post: The perfect Nullstellensatz just got more perfect","author":"Shalit Orr","year":"2019","unstructured":"Orr Shalit. 2019. Blog post: The perfect Nullstellensatz just got more perfect. https:\/\/noncommutativeanalysis.wordpress.com\/2019\/06\/20\/the-perfect-nullstellensatz-just-got-more-perfect\/ visited on 21.04.2026."},{"key":"e_1_3_3_2_37_2","unstructured":"Grigori\u00a0S. Tseitin. 1958. An associative calculus with an insoluble problem of equivalence. Trudy Mat. Inst. Steklov 52 (1958) 172\u2013189. In Russian. Translation in [30]."},{"key":"e_1_3_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-75326-8_21"},{"key":"e_1_3_3_2_39_2","unstructured":"Xingqiang Xiu. 2012. Non-commutative Gr\u00f6bner Bases and Applications. Ph.\u00a0D. Dissertation. University of Passau Germany. Available at http:\/\/www.opus-bayern.de\/uni-passau\/volltexte\/2012\/2682\/."},{"key":"e_1_3_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597066.3597067"}],"event":{"name":"ISSAC '26: 51st International Symposium on Symbolic and Algebraic Computation","location":"Oldenburg , Germany","acronym":"ISSAC '26"},"container-title":["Proceedings of the 2026 International Symposium on Symbolic and Algebraic Computation"],"original-title":[],"deposited":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T16:23:55Z","timestamp":1783614235000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3815436.3815447"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,12]]},"references-count":39,"alternative-id":["10.1145\/3815436.3815447","10.1145\/3815436"],"URL":"https:\/\/doi.org\/10.1145\/3815436.3815447","relation":{},"subject":[],"published":{"date-parts":[[2026,7,12]]},"assertion":[{"value":"2026-07-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}