How to automatise proofs of operator statements: Moore-Penrose inverse -- a case study

Klara Bernauer, Clemens Hofstadler, Georg Regensburger

We describe a recently developed algebraic framework for proving first-order statements about linear operators by computations with noncommutative polynomials. Furthermore, we pres…