An idealized strategy is an iterative procedure which would invoke Categorize on the pair of sets of polynomial equations C and ( is initially empty), allow creation of motivated unknowns, allow for unknowns to be redeclared as knowns and allow for human intervention. Human intervention would consist of selecting particular equations which are nice in some way (e.g., this is a Ricatti equation), adding them to the collection and possibly selecting a motivated unknown y as described above. This procedure would terminate when the ideal generated by equals the ideal generated by . This, of course, is equivalent to the condition that is empty for each . In other words, an idealized strategy terminates when all of the polynomial equations which can be derived algebraically and involve unknowns can be derived algebraically from the equations in together with the equations which do not involve unknowns.
If the reader would indulge us, we now discuss a more visual way of thinking about idealized strategies. For ease of exposition, the discussion in this paragraph will ignore the possibility of introducing motivated unknowns, the redeclaration of unknowns as knowns or human intervention. For each pair of collections of polynomials C and , suppose that one has an idealized display:
When one begins using an idealized strategy, C would be the collections of equations coming from the problem at hand and would be initially empty. During each iteration of a strategy, one would choose a number of polynomials from the ideal generated by , (that is, below the dark line) and place them in (that is, above the dark line). The idealized display would then adjust itself so that what appears in above the line and what appears below the line corresponds to the new value of . When there are no equations below the dark line, the idealized strategy is complete. If and, for , is produced from C and using one step of an idealized strategy and each equation which is in but not in has at most 1 (motivated) unknown, then we say that is derivable from C by an idealized strategy.
A question about strategies is
Which classical results can be derived using an idealized strategy?
This question gives an abstract statement of what we address in this paper.
One intends, of course, to move beyond this question to the derivation of new theorems. However, in the early stages of the subject, we think that the most urgent task is to understand classical theorems from this viewpoint. Evaluating these new and unusual techniques on a new and not well understood problem gives less of an idea of their strength than evaluating them on a well understood problem. Typically, if we derive a new theorem using symbol manipulation, then one can go back and produce a proof by hand, using ideas gotten from the symbolic manipulation.