Rewrite Rules and Simplification of Matrix Expressions
John J. Wavrik · 1996
This paper concerns the automated simplification of expressions which involve non-commuting variables. The technology has been applied to the simplification of matrix and operator theory expressions which arise in engineering applications. The non-commutative variant of the Grobner Basis Algorithm is used to generate rewrite rules. We will also look at the phenomenon of infinite bases and implications for automated theorem proving.