Algebraic First-Order Theorem Proving

Algebraic techniques, such as Gröbner bases, have a long and successful history in automatic geometric theorem proving. Recently, these methods have found a new and promising area of application in the context of proving operator statements. Operator statements are first-order formulas involving identities of matrices or, more generally, linear operators. These statements appear in various branches of mathematics, such as linear algebra, geometry, and functional analysis, as well as in related disciplines like signal processing or quantum physics.

In this talk, we present how the correctness of a first-order operator statement can be translated into an algebraic statement about noncommutative polynomials, which can be verified automatically using computer algebra. More precisely, this translation gives rise to a semi-decision procedure that allows to prove any true operator statement based on a single algebraic computation. Moreover, we discuss how this algebraic framework can be leveraged to compute shortest proofs of operator statements. For false operator statements, we address how to certify their invalidity by constructing explicit counterexamples. While this is an undecidable problem in general, we present a heuristic method that has shown promising results so far.