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 ncalg@osiris.ucsd.edu 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 ncalg@osiris.ucsd.edu. 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.

- Background on polynomial equations and Ideals
- A highly idealized picture
- A practical picture
- Algorithms and their properties
- A practical notation
- Computational concerns
- Acknowledgements

Wed Jul 3 10:27:42 PDT 1996