The objective of this paper is two-fold. First we present a methodology for using a combination of computer assistance and human intervention to discover highly algebraic theorems in operator, matrix, and linear systems engineering theory. Since the methodology allows limited human intervention, it is slightly less rigid than an algorithm. We call it a strategy. The second objective is to illustrate the methodology by deriving four theorems. The presentation of the methodology is carried out in three steps. The first step is introducing an abstraction of the methodology which we call an idealized strategy. This abstraction facilitates a high level discussion of the ideas involved. Idealized strategies cannot be implemented on a computer. The second and third steps introduce approximations of these abstractions which we call prestrategy and strategy, respectively. A strategy is more general than a prestrategy and, in fact, every prestrategy is a strategy. The above mentioned approximations are implemented on a computer. We stress that, since there is a computer implementation, the reader can use these techniques to attack their own algebra problems. Thus the paper might be of both practical and theoretical interest to analysts, engineers, and algebraists. Now we give the idea of a prestrategy. A prestrategy relies almost entirely on two commands which we call NCProcess1 and NCProcess2. These two commands are sufficiently powerful so that, in many cases, when one applies them repeatedly to a complicated collection of equations, they transform the collection of equations into an equivalent but substantially simpler collection of equations. A loose description of a prestrategy applied to a list of equations is:
(1) Declare which variables are known and which are unknown. At the beginning of a prestrategy, the order in which the equations are listed is not important, since NCProcess1 and NCProcess2 will reorder them so that the simplest ones appear first.
(2) Apply NCProcess1 to the equations; the output is a set of equations, usually some in fewer unknowns than before, carefully partitioned based upon which unknowns they contain.
(3) The user must select ``important equations,'' especially any which solve for an unknown, say x.