Symbolic computations for identities of linear operators

Many processes in science and engineering can be modeled by so-called linear functional systems. To manipulate and analyze such systems, one computes with the corresponding matrices and linear operators. Properties of systems and operators are expressed by identities. Instead of working with concrete matrices and operators, symbolic computation works with mathematical objects represented by symbols. The main goal of the project Symbolic computations for identities of linear operators is to automatize such formal computations with operators and classes of systems beyond what is currently possible on the computer. In particular, we are interested in symbolic methods and computer algebra tools for proving and discovering identities of linear operators and for solving operator equations. In the project, we develop methods to analyze classes of dynamical systems in engineered processes and their control. These systems and their transformations are usually modeled by differential, delay, and integral operators. To compute with such operators, we work out a unique way of representing them. Based on these normal forms, we will prove and discover identities of operators automatically by computer algebra software, which we develop in the course of the project. If input and output of operators or matrices have different dimensions, they cannot be added and composed in arbitrary ways. This restricts computations with operators and matrices. In the project, we will work out new symbolic methods to deal with these restrictions. The idea is to first compute symbolically without restrictions and then justify the result independent of how it was obtained.

Many processes in science and engineering can be modeled using linear systems of so-called functional equations. To handle and analyze such systems, computations with the corresponding matrices and linear operators are performed. Many important properties of systems and operators can be described by equations. In computer algebra, symbols representing the mathematical objects and their associated equations are used. The goal of the project "Symbolic computations for identities of linear operators" was to automate these formal computations with operators and classes of systems beyond what was previously possible using computers. Automated proofs and discoveries of operator equations lie at the intersection of computer algebra and artificial intelligence. A central result of the project is a general framework for automated proofs of statements about identities of linear operators using computations with noncommutative polynomials. The publications cover all aspects of this approach, including the logical and algebraic foundations, new algorithms, heuristic considerations, efficient implementations, freely available software packages, and comprehensive case studies. We were able to prove numerous classical results about generalized inverses as well as results from current research papers in a few seconds with our software. Together with our collaborators, we also found and proved new results about so-called Moore-Penrose inverses using computer assistance. An important aspect of our approach is that for every true statement about identities of operators, a certificate is computed that can be easily verified independently of our software. In this sense, the developed method is theoretically complete. Thanks to new algorithms, heuristic considerations, and efficient implementation, the software can also provide proofs for current research questions concerning linear operators in practice. Another research focus of the project was identities of linear operators from analysis, such as differentiation, integration, and evaluations. We describe all algebraic equations that these operators satisfy in a current publication in a leading mathematics journal. In particular, we show that twelve rewrite rules are sufficient to simplify any expression to a unique normal form. For the computer-assisted proof of the completeness of these rules, we developed a new theoretical approach and our own software. With these rewrite rules, classical identities from analysis and results for systems of linear differential equations can be proven algebraically. Additionally, the algebraic approach allows for generalizations of the Taylor formula and shuffle relations for nested integrals to functions with singularities, as they arise for example in theoretical physics for calculations in quantum field theories.