Formal proofs of operator identities by a single formal computation

DOI10.1016/j.jpaa.2020.106564zbMath1486.68259arXiv1910.06165OpenAlexW4286683942WikidataQ113870190 ScholiaQ113870190MaRDI QIDQ2223357

Jamal Hossein Poor, Georg Regensburger, Clemens G. Raab

Publication date: 28 January 2021

Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1910.06165

zbMATH Keywords

quiver representationslinear categoriesnoncommutative polynomialsmatrix identitiesalgebraic operator identities

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Category-theoretic methods and results in associative algebras (except as in 16D90) (16B50) Representations of quivers and partially ordered sets (16G20) Ideals of polynomials and of multilinear mappings in operator theory (47L22)

Related Items

Signature Gröbner bases, bases of syzygies and cofactor reconstruction in the free algebra ⋮ Signature Gröbner bases in free algebras over rings ⋮ Computing elements of certain form in ideals to prove properties of operators ⋮ Algebraic proof methods for identities of matrices and operators: improvements of Hartwig's triple reverse order law

Uses Software

• OperatorGB
• Letterplace

Cites Work

• Unnamed Item
• Unnamed Item
• The diamond lemma for ring theory
• Computer assistance for ``discovering formulas in system engineering and operator theory
• An introduction to commutative and noncommutative Gröbner bases
• Formally verifying proofs for algebraic identities of matrices
• Convergent presentations and polygraphic resolutions of associative algebras
• Algebraic properties of generalized inverses
• Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
• Gröbner-Shirshov Bases for Categories
• Solving Polynomial Equation Systems
• Standard Gröbner-Shirshov Bases of Free Algebras Over Rings, I
• On Deriving the Inverse of a Sum of Matrices
• Computer simplification of formulas in linear systems theory
• HOMOLOGICAL ALGEBRA OF TWISTED QUIVER BUNDLES
• Compatible rewriting of noncommutative polynomials for proving operator identities
• Certifying operator identities via noncommutative Gröbner bases
• Using noncommutative Gröbner bases in solving partially prescribed matrix inverse completion problems

This page was built for publication: Formal proofs of operator identities by a single formal computation