next up previous contents
Next: Example: The Bart-Gohberg-Kaashoek-Van Dooren Up: Prestrategy Previous: Prestrategy

When to stop; the end game

The prestrategy described above is a loop and we now discuss when to exit the loop.

The digested equations (those in items O1, O2 and O3) often contain the necessary conditions of the desired theorem and the main flow of the proof of the converse. If the starting polynomial equations follow as algebraic consequences of the digested equations, then we should exit the above loop. The starting equations, say tex2html_wrap_inline4780 , follow as algebraic consequences of the digested equations, say tex2html_wrap_inline4782 , if and only if the Gröbner Basis generated by tex2html_wrap_inline4784 reduces (in a standard way) the polynomial tex2html_wrap_inline4786 to 0 for tex2html_wrap_inline4788 . Checking whether or not this happens is a purely mechanical process. (See §).

When one exits the above loop, one is presented with the question of how to finish of the proof of the theorem. We shall call the steps required to go from a final spreadsheet to the actual theorem the ``end game''. We shall describe some ``end game'' technique in §. We shall illustrate the ``end game'' in § and §. As we shall see, typically the first step is to run NCProcess2 whose output is a very small set of equations.

Wed Jul 3 10:27:42 PDT 1996