{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T03:11:32Z","timestamp":1783653092265,"version":"3.55.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030535179","type":"print"},{"value":"9783030535186","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_14","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"222-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formally Verifying Proofs for Algebraic Identities of Matrices"],"prefix":"10.1007","author":[{"given":"Leonard","family":"Schmitz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Levandovskyy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1016\/0001-8708(78)90010-5","volume":"29","author":"G Bergman","year":"1978","unstructured":"Bergman, G.: The diamond lemma for ring theory. Adv. Math. 29, 178\u2013218 (1978)","journal-title":"Adv. Math."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Chenavier, C., Hofstadler, C., Raab, C.G., Regensburger, G.: Compatible rewriting of noncommutative polynomials for proving operator identities. https:\/\/arxiv.org\/abs\/2002.03626 (2020)","DOI":"10.1145\/3373207.3404047"},{"issue":"1","key":"14_CR3","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S144678870800044X","volume":"86","author":"T Damm","year":"2009","unstructured":"Damm, T., Wimmer, H.K.: A cancellation property of the Moore-Penrose inverse of triple products. J. Aust. Math. Soc. 86(1), 33\u201344 (2009)","journal-title":"J. Aust. Math. Soc."},{"key":"14_CR4","unstructured":"Decker, W., Greuel, G.M., Pfister, G., Sch\u00f6nemann, H.: Singular 4-1-3 \u2013 A computer algebra system for polynomial computations (2020). http:\/\/www.singular.uni-kl.de"},{"issue":"9","key":"14_CR5","doi-asserted-by":"publisher","first-page":"1561","DOI":"10.1016\/j.aml.2011.03.046","volume":"24","author":"CY Deng","year":"2011","unstructured":"Deng, C.Y.: A generalization of the Sherman-Morrison-Woodbury formula. Appl. Math. Lett. 24(9), 1561\u20131564 (2011)","journal-title":"Appl. Math. Lett."},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-21046-4_3","volume-title":"Automated Deduction in Geometry","author":"B Gr\u00e9goire","year":"2011","unstructured":"Gr\u00e9goire, B., Pottier, L., Th\u00e9ry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol. 6301, pp. 42\u201359. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21046-4_3"},{"key":"14_CR7","unstructured":"Helton, J., Kronewitter, F.: Computer algebra in the control of singularly perturbed dynamical systems (1999). http:\/\/math.ucsd.edu\/~ncalg\/DELL\/SingPert\/singpertcdc99.pdf"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/3371991.3371996","volume":"53","author":"C Hofstadler","year":"2019","unstructured":"Hofstadler, C., Raab, C.G., Regensburger, G.: Certifying operator identities via noncommutative Gr\u00f6bner bases. ACM Commun. Comput. Algebra 53, 49\u201352 (2019)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"14_CR9","unstructured":"Joswig, M., Fieker, C., Horn, M., et al.: The oscar project (2020). https:\/\/oscar.computeralgebra.de"},{"issue":"1\u20133","key":"14_CR10","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0024-3795(01)00382-2","volume":"338","author":"FD Kronewitter","year":"2001","unstructured":"Kronewitter, F.D.: Using noncommutative Gr\u00f6bner bases in solving partially prescribed matrix inverse completion problems. Linear Algebra Appl. 338(1\u20133), 171\u2013199 (2001)","journal-title":"Linear Algebra Appl."},{"key":"14_CR11","unstructured":"Levandovskyy, V., Abou Zeid, K., Sch\u00f6nemann, H.: Singular: Letterplace \u2013 A singular 4-1-3 subsystem for non-commutative finitely presented algebras (2020). http:\/\/www.singular.uni-kl.de"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/3-540-51084-2_14","volume-title":"Symbolic and Algebraic Computation","author":"T Mora","year":"1989","unstructured":"Mora, T.: Groebner bases in non-commutative algebras. In: Gianni, P. (ed.) ISSAC 1988. LNCS, vol. 358, pp. 150\u2013161. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51084-2_14"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0304-3975(94)90283-6","volume":"134","author":"T Mora","year":"1994","unstructured":"Mora, T.: An introduction to commutative and non-commutative Gr\u00f6bner bases. Theor. Comput. Sci. 134, 131\u2013173 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316271902","volume-title":"Solving Polynomial Equation Systems IV: vol. 4. Buchberger Theory and Beyond","author":"T Mora","year":"2016","unstructured":"Mora, T.: Solving Polynomial Equation Systems IV: vol. 4. Buchberger Theory and Beyond. Cambridge University Press, Cambridge (2016)"},{"issue":"1","key":"14_CR15","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1006\/jsco.1996.0040","volume":"22","author":"FL Pritchard","year":"1996","unstructured":"Pritchard, F.L.: The ideal membership problem in non-commutative polynomial rings. J. Symb. Comput. 22(1), 27\u201348 (1996)","journal-title":"J. Symb. Comput."},{"key":"14_CR16","unstructured":"Raab, C.G., Regensburger, G., Poor, J.H.: Formal proofs of operator identities by a single formal computation. https:\/\/arxiv.org\/abs\/1910.06165 (2019)"},{"key":"14_CR17","unstructured":"Stein, W., et al.: Sage Mathematics Software. The Sage Development Team (2020)"},{"issue":"3","key":"14_CR18","first-page":"360","volume":"4","author":"JJ Wavrik","year":"1996","unstructured":"Wavrik, J.J.: Rewrite rules and simplification of matrix expressions. Comput. Sci. J. Moldova 4(3), 360\u2013398 (1996)","journal-title":"Comput. Sci. J. Moldova"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Youla, D.C., Jabr, H.A., Bongiorno, J.J.: Modern Wiener-Hopf design of optimal controllers. II: the multivariable case. IEEE Trans. Autom. Control 21 319\u2013338 (1976)","DOI":"10.1109\/TAC.1976.1101223"},{"key":"14_CR20","volume-title":"Robust and Optimal Control","author":"K Zhou","year":"1996","unstructured":"Zhou, K., Doyle, J.C., Glover, K.: Robust and Optimal Control. Prentice Hall, Upper Saddle River (1996)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53518-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,23]],"date-time":"2021-04-23T23:18:57Z","timestamp":1619219937000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}