next up previous contents
Next: Appendix to Part I: Up: Strategies and Applications Previous: Monomial orders


Let us review the basic ideas. We start with knowns and unknowns and a set C of polynomial equations. As a strategy proceeds, more and more equations are digested by the user and placed in a set tex2html_wrap_inline4190 . Also, more and more unknowns become knowns. Thus we ultimately have two classes of knowns: original knowns tex2html_wrap_inline6224 and user designated knowns tex2html_wrap_inline6226 .

Often prominent in the statement of a theorem is the subset tex2html_wrap_inline6228 of tex2html_wrap_inline4190 consisting of equations involving only knowns tex2html_wrap_inline6232 .

Indeed many classical theorems (at least the ones we present here) have the form:

the equations in C have a solution if and only if the equations in tex2html_wrap_inline6228 have a solution

Now the ``only if'' part of this is clear from the derivation using a strategy, but proving the ``if'' part is a less precise process. Proving the ''if'' part is the business of what we call the ``end game'', which is the act of using the last spreadsheet generated during a prestrategy to write down a theorem and its proof. Clearly one of the first steps is to translate the equations on the spreadsheet into palatable language. For example, if one obtains the equation tex2html_wrap_inline6238 and tex2html_wrap_inline4062 and tex2html_wrap_inline6242 , then one would say that P is a projection. A slightly more complicated example would be if tex2html_wrap_inline6246 where tex2html_wrap_inline5602 , tex2html_wrap_inline5604 , tex2html_wrap_inline5606 and Y are invertible and tex2html_wrap_inline6256 and tex2html_wrap_inline5606 was self-adjoint. If tex2html_wrap_inline5746 and X were in tex2html_wrap_inline6264 , then one could say that tex2html_wrap_inline5766 would have to be both symmetric and invertible.

When one performs the approach of the above paragraph to obtain the ``if'' part of the theorem, one tries to record enough necessary conditions so that the conditions are also sufficient. Once such conditions (in the form of polynomial equations) are selected from the spreadsheetgif, then one assumes that each of these equations hold for certain unspecified values of the knowns (those variables in tex2html_wrap_inline6264 ) and tries to find values for the remaining variables such that each of the equations on the final spreadsheet holds. If one can find values for these remaining variables, then, since each of the equations of the final spreadsheet holds, each of the equations on the initial spreadsheet holds and one has proven the desired ``if'' part of the theorem. Fortunately, the spreadsheet often has a block triangular form which is amenable to backsolving. One of the benefits of putting the equations in categories is that this reveals this triangular structure (see §).

These ``end game'' techniques are demonstrated in § and §.

next up previous contents
Next: Appendix to Part I: Up: Strategies and Applications Previous: Monomial orders

Wed Jul 3 10:27:42 PDT 1996