The equations mentioned above take the form of a polynomial , with matrices or operators substituted for the variables, set equal to zero.
Vast experience with the commuting case of the manipulation of collections of equations suggests that using a noncommutative Gröbner Basis algorithm is an essential tool for analyzing systems of equations.
We wish to stress that one does not need to know a theorem in order to ``discover'' it using the techniques in this paper. Furthermore, any method which assumes that all of the hypotheses are known at the beginning of the computation or that all of the hypotheses can be stated algebraically will be of limited practical use. For example, since the Gröbner Basis algorithm only discovers polynomial equations which are algebraically true and not those which require analysis or topology, the use of this algorithm alone has a limited use. Insights gained from analysis during a computer session could be added as (algebraic) hypotheses while the session is in progress. Decisions can take a variety of forms and can involve recognizing a Ricatti equation, recognizing that a particular square matrix is onto and so invertible, recognizing that a particular theorem now applies to the problem, etc. The user would then have to record and justify these decisions independently of the computer run. While a strategy allows for human intervention, the intervention must follow certain rigid rules for the computer session to be considered a strategy.
One thing to bear in mind when reading the examples in this paper is that they present not just proofs but also the methods for discovering proofs. This makes their presentation longer than the mere presentation of the slickest known proof. Also, to a specialist, some of the examples have the feel of a ``back of the envelope computation''.
The software which was developed for this paper is freely available (send electronic mail to firstname.lastname@example.org for more information). The code is accessed through Mathematica. The bulk of the computations are performed by the C++ code which is invisible to the user. The output is automatically displayed to the screen. The output is formatted using the program LaTeX. As of December 1995, the code is too slow to run interactively for most problems. As more of the code is moved into C++, it will become dramatically faster. Also, one would probably want to use this software in conjunction with NCAlgebra which is the main Mathematica package for doing noncommutative algebraic computations. NCAlgebra is also available from email@example.com. This extensive software makes these techniques available for exploration of a new and unusual type of question in operator theory or systems engineering: which classical theorems in operator theory or systems theory can be ``discovered'' using a strategy? Of course we hope new theorems will be discovered, but the best place to evaluate these ideas is on the classics.