Formally verifying proofs for algebraic identities of matrices

DOI10.1007/978-3-030-53518-6_14MaRDI QIDQ2219403zbMATH OpenOpenAlexFDO

Authors Leonard Schmitz, V. Levandovskyy

Publication date 20 January 2021

Full work available at URL https://doi.org/10.1007/978-3-030-53518-6_14

zbMATH Keywords

proof assistantelimination theorymatrix identitiesword problemsproof certificatesGröbner bases

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Matrix equations and identities (15A24) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Algebraic proof methods for identities of matrices and operators: improvements of Hartwig's triple reverse order law
• Computer simplification of formulas in linear systems theory
• Computer proofs for polynomial identities in arbitrary many variables
• COMPUTER PROOFS OF MATRIX PRODUCT IDENTITIES
• Formal proofs of operator identities by a single formal computation

Cited in

(10)

• Formal proofs of operator identities by a single formal computation
• How to Automatise Proofs of Operator Statements: Moore–Penrose Inverse; A Case Study
• 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
• Computer algebra procedures for verifying the definiteness of a matrix on a subspace
• Short proofs of ideal membership
• Letterplace
• Signature Gröbner bases, bases of syzygies and cofactor reconstruction in the free algebra
• Certifying operator identities via noncommutative Gröbner bases
• Signature Gröbner bases in free algebras over rings

Describes a project that uses

Uses Software

• SageMath
• SINGULAR
• OSCAR

This page was built for publication: Formally verifying proofs for algebraic identities of matrices

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2219403)