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.