next up previous contents
Next: Background on polynomial equations Up: Strategies and Applications Previous: Strategies and Applications

Introduction

The goal in this paper is to describe and illustrate a highly computer assisted method for discovering certain types of theorems. Many theorems in operator theory and engineering systems theory amount to giving hypotheses under which it is possible to solve large collections of equations. At the beginning of ``discovering'' a theorem, the problem is to determine the nature of solutions to a large collection of equations. Discovering a theorem involves exploring the consequences of these equations until a simpler equivalent set of equations is found.

The equations mentioned above take the form of a polynomial gif, 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. gif 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. gif 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.




next up previous contents
Next: Background on polynomial equations Up: Strategies and Applications Previous: Strategies and Applications

Helton
Wed Jul 3 10:27:42 PDT 1996