Gröbner Bases:
Tutorial for Newcomers

Bruno Buchberger
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria

Special Semester on Gröbner Bases
RICAM / RISC,Linz,Austria
April 30, 2006

Copyright Bruno Buchberger 2006

Copyright Note: This file may be copied, stored, and distributed subject to the following conditions:

- The file is kept unchanged and complete including this copyright note.
- A message is sent to bruno.buchberger@jku.at.
- If the material is used, this talk should be cited appropriately.

Motivation

The notion of Gröbner bases, the main theorem on characterizing Gröbner bases, an algorithm for constructing Gröbner bases, and first applications have been introduced in BB's PhD thesis 1995 (aequ. math. 1970).

Dozens of (difficult) problems turned out to be reducible to the construction of Gröbner bases. (~ 1000 papers, 10 textbooks, entry 13P10 in AMS index).

This is based on the fact that Gröbner bases have many nice properties (e.g. canonicality property, elimination property, syzygy problem).

For the construction of Gröbner bases we have an algorithm.

General strategy: Hence, problems for arbitrary polynomial sets F can often be solved by constructing a corresponding Gröbner basis G and solving the problems for G.

A "beautiful" theory: The notion of Gröbner bases and the algorithm is easy to explain, but correctness is based on a non-trivial theory.

A very active research area: more efficient algorithms based on more theory,  and more applications.

The Special Semester 2006 addresses a few topical areas of Gröbner bases research (theory and applications) in detail, see the various Workshops scheduled.

Earlier, in 1998, we organized a Special Conference on Gröbner bases at RISC, see

This talk is based on the paper  BB, "Introduction to Gröbner Bases", pp. 3-31, in this book. Will be distributed to participants of Workshops D1, D2, D3, also downloadable form the web site.

The presentation in the paper is more formal.

This talk is also downloadable from the web site.

The Linear Combination of Polynomials

(Subscript[f, 1])=-2 y+x y
(Subscript[f, 2])=-(x^2)+(y^2)

Leading power products: w.r.t. an ordering of the power products (e.g. lexicographically, by total degreee or ...)

(There are infinitely many "admissible" orderings for Gröbner bases theory that can be characterized by two easy axioms.)

Consider now the following linear combination of (Subscript[f, 1]) and (Subscript[f, 2]):

g = (y) (Subscript[f, 1]) +  (-x + 2) (Subscript[f, 2])

g = (y) (Subscript[f, 1]) +  (-x + 2) (Subscript[f, 2])  // Expand

Observation:  The leading power product   (x^3)   of g is 
     neither a multiple of the leading power product    x y     of (Subscript[f, 1])
     nor      a multiple of the leading power product      (y^2)    of (Subscript[f, 2]).

Definition of Groebner Bases (BB 1965, Gordon 1899)

A set F of polynomials is called a Groebner basis (w.r.t. the chosen ordering of power products) iff the above phenomenon cannot happen, i.e. iff
     for all (Subscript[f, 1]),...,(Subscript[f, m])∈ F and all polynomials (Subscript[h, 1]),...,(Subscript[h, m]),
          the leading power product of  (Subscript[h, 1]) (Subscript[f, 1]) +  ...   +  
        (Subscript[h, m]) (Subscript[f, m]) 
          is a multiple of the leading power product of 
               at least one of the polynomials in F.

Counterexample: The Set F = {(Subscript[f, 1]), (Subscript[f, 2])} of the Above Example is not a Groebner basis.

Example of a Groebner Basis

The following set G (results from F by adding -2 (x^2) + (x^3)) is a Groebner basis:

G = {-2 (x^2) + (x^3), -2 y + x y, -(x^2) + 
          (y^2)}

For example,

(1 + 3  y) (-2 (x^2) + (x^3)) + (8  x + 
              3  x y) (-2 y + x y) + (2 - x - 
              (y^2)) (-(x^2) + (y^2)) // Expand

(1) (-2 (x^2) + (x^3)) + (8  x) (-2 y + 
              x y) + (y) (-(x^2) + (y^2)) // Expand

Why is it difficult to check whether a given F is a Groebner basis?

How can we check whether a given F is a Groebner basis?

How can we get an "equivalent" Groebner basis G for a given F (which may not be a Groebner basis)?

The "Main Theorem" of Algorithmic Gröbner Bases Theory (BB 1965):

F is a Gröbner basis  ⟺   (Underscript[∀ , (Subscript[f, 1]), (Subscript[f, 2]) ∈ F])  remainder[ F, S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]] = 0.

Proof: Nontrivial. Combinatorial. Some details later. See paper in BB, Winkler, 1998, for a modern version.

The theorem reduces an infinite check to a finite check:  Recall definition of "F is a Gröbner basis":

for all (Subscript[f, 1]),...,(Subscript[f, m])∈ F and polynomials (Subscript[h, 1]),...,(Subscript[h, m]),
          the leading power product of  (Subscript[h, 1]) (Subscript[f, 1]) +  ...   +  
        (Subscript[h, m]) (Subscript[f, m]) 
          is a multiple of the leading power product of at least one of the polynomials in F.

The power of the Gröbner bases method is contained in this theorem and its proof.

S-Polynomials

(Subscript[f, 1])=-2 y+x y
(Subscript[f, 2])=-(x^2)+(y^2)

S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]=y  (Subscript[f, 1])-x  (Subscript[f, 2])

S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]=y  (Subscript[f, 1])-x  (Subscript[f, 2])       //Expand

The Algorithm 'remainder'

Roughly, remainder[ F, g] results from replacing power products in g by a lower products using the polynomials in F until no more replacements are possible.

Example:

Consider, again,

(Subscript[f, 1]) = -2 (x^2) + (x^3);
(Subscript[f, 2]) = -2 y + x y;
(Subscript[f, 3]) = -(x^2) + (y^2);

F = {(Subscript[f, 1]), (Subscript[f, 2]), (Subscript[f, 3])};

and

g = x y - 3 x (y^2);

A "reduction" ("division") step on g w.r.t. F:

(Subscript[g, 1]) = g  + (3 x) (Subscript[f, 3])

(Subscript[g, 1]) = g  + (3 x) (Subscript[f, 3]) // Expand

A next division step w.r.t. F:

F = {(Subscript[f, 1]), (Subscript[f, 2]), (Subscript[f, 3])}

(Subscript[g, 2]) = (Subscript[g, 1])  + (-1) (Subscript[f, 2])  // Expand

A next division step w.r.t. F:

F = {(Subscript[f, 1]), (Subscript[f, 2]), (Subscript[f, 3])}

(Subscript[g, 3]) = (Subscript[g, 2])  + (3) (Subscript[f, 1])  // Expand

This is the remainder of the division of g w.r.t. F because ...

Remainder Algorithms are Available in all Math Systems

PolynomialReduce[g, F, {y, x}]

Note: the remaindering algorithm can be extended to a "remaindering with co-factors":

g  -  
        0    (-2 (x^2) + (x^3))   -  (1 - 
              3 y)  (  -2 y + 
              x y)   -   (-6 ) (-(x^2) + (y^2))  //  
      Expand

Now We Can Check Groebnerianity

Let's again look to the above example:

F = {(Subscript[f, 1]), (Subscript[f, 2]), (Subscript[f, 3])}

PolynomialReduce[(Subscript[f, 1]) y  -  (Subscript[f, 2]) (x^2), F, {y, x}]

PolynomialReduce[(Subscript[f, 1]) (y^2)  -  (Subscript[f, 3]) (x^3), F, {y, x}]

PolynomialReduce[(Subscript[f, 2]) y  -  (Subscript[f, 3]) x, F, {y, x}]

The Problem of Constructing Gröbner Bases

Given F,  find G   s.t. Ideal(F) = Ideal(G) and G is a Gröbner basis.

(Ideal(F) := the set of all linear combinations  (Subscript[h, 1]) (Subscript[f, 1]) +  ...   +  
        (Subscript[h, m]) (Subscript[f, m]) 
                 
                with (Subscript[f, 1]), ..., (Subscript[f, m]) ∈ F and  (Subscript[h, 1]),...,(Subscript[h, m]) arbitrary polynomials.)

An Algorithm for Constructing Gröbner Bases (BB 1965)

Recall the main theorem:

F is a Gröbner basis   ⟺    (Underscript[∀ , (Subscript[f, 1]), (Subscript[f, 2]) ∈ F])  remainder[ F, S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]] = 0.

Based on the main theorem, the problem can be solved by the following algorithm:

Start with G:= F. 
For any pair of polynomials (Subscript[f, 1]), (Subscript[f, 2]) ∈ G:

      h := remainder[ G, S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]] 
      
      If h = 0, consider the next pair.
      
      If h ≠ 0, add h to G and iterate.

The algorithm allows many refinements and variants which, however, are all based on the notion of S-polynomial and variants of the main theorem.

Correctness and Termination of the Algorithm

Correctness: Easy as soon as we know the main theorem.

Termination: by Dickson's Lemma (Dickson 1913, BB 1970).

A sequence  (Subscript[p, 1]),  (Subscript[p, 2]),   ...   of power products with the property that, for all i < j, (Subscript[p, i]) does not divide (Subscript[p, j]), must be finite.

Specializations

The Gröbner bases algorithm,

        for linear polynomials, specializes to Gauss' algorithm, and

        for univariate polynomials, specializes to Euclid's algorithm.

Example

Let's again look at

(Subscript[f, 1])=-2 y+x y
(Subscript[f, 2])=-(x^2)+(y^2)

F = {(Subscript[f, 1]), (Subscript[f, 2])}

F is not a Groebner basis.

The S-polynomial of (Subscript[f, 1]), (Subscript[f, 2]):

S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]=y  (Subscript[f, 1])-x  (Subscript[f, 2])       //Expand

Its remainder w.r.t. F is:

-2 (x^2) + (x^3).

All the other S-polynomials have remainder 0. Hence, we arrived at a Groebner basis.

The Groebner basis algorithm is available now available in all math software systems, e.g. in Mathematica:

G = GroebnerBasis[F, {y, x}]

Reduced Gröbner Bases

A set F of polynomials is called a reduced Gröbner basis (w.r.t. the chosen ordering of power products) iff 
    F is a Gröbner bases and,
    for all f ∈ F, 
         remainder[ F-{f}, f] = f and
         f is monic.

Algorithm for obtaining a reduced Gröbner basis: Compute a Gröbner basis and then "auto-reduce" the basis.

Extended Gröbner Basis Algorithm

Keeps track of how the polynomials in the Gröbner basis G can be linearly combined from the polynomials in F.

Applications are Based on Three Main Properties of Gröbner Bases

Canonicality Property

Elimination Property

Syzygy Property

Canonicality

Remaindering modulo a Gröbner basis F is a "canonical simplifier" for congruence modulo F:

\(TraditionalForm\`f\( ≡ \_F\)g\ \ ⟺\ \ remainder[F, f] = remainder[F, g]\)

f  (Subscript[≡ , F  ])remainder[
          F, f]

"Second order" canonicality:  "Reduced Gröbner basis" is a "canonical simplifier" for "have same congruence":

\(TraditionalForm\`Ideal[
          F]\  = \ \(\(Ideal[
              G]\ \ ⟺\ \ reduced–Gröbner–basis[F]\)\(=\)\)\)reduced–Gröbner–basis[G]

Ideal[F] = Ideal[ reduced–Gröbner–basis[F] ].

Elimination Ideals

Let ≺ be the lexicographic ordering defined by \(TraditionalForm\`\(\(x\_1\)\(\ \)\(≺\)\(\ \)\(x\_2\)\(\ \ \)\)\)≺ ... ≺ (Subscript[x, n]). If F is a Gröbner basis w.r.t. ≺, then

If F is a Gröbner basis w.r.t. ≺    then, for all  i ≤ n,

Ideal[F] ⋂  K[(Subscript[x, 1]),…,(Subscript[x, i])] =  Ideal[  F ⋂  K[(Subscript[x, 1]),…,(Subscript[x, i])] ]

The "elimination ideals" of an ideal can be easily computed if we have a Gröbner basis for the ideal.

Syzygy Property (Linear Syzygies)

Given a tuple ⟨ (Subscript[f, 1]),  …,  (Subscript[f, m])⟩ of polynomials. How can we obtain a finite basis for the set of all possible polynomial solutions ("syzygies")  ⟨ (Subscript[h, 1]),  …,  (Subscript[h, m])⟩ of the linear diophantine equation

\(TraditionalForm\`\(\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \)\(h\_\(\(1\)\(\ \)\) . \ \ f\_\(\(1\)\(\ \)\) + \ \ …\ \  + \ 
        h\_m\  . \ f\_m\ \  = \ \ \(\(0\)\(\ \ \ \ \)\(?\)\)\)\)\)

In the case that F:= { (Subscript[f, 1]),  …,  (Subscript[f, m])} is a Gröbner basis the following set of tuples is a finite basis for the infinite set of all  syzgies:

consider all pairs  (Subscript[f, i]), (Subscript[f, j]) :

m := LCM[ LPP[ (Subscript[f, i]) ], LPP[ (Subscript[f, j])]],  (Subscript[u, i]) :=  m / LPP[(Subscript[f, i])],    (Subscript[u, j]) := m / LPP[(Subscript[f, j])]

⟨ (Subscript[H, 1]),  …,  (Subscript[H, m])⟩ :=  the cofactors obtained by remaindering 
                                                  S-polynomial[ (Subscript[f, i]), (Subscript[f, j])] modulo F

⟨ (Subscript[h, 1]),  …,  (Subscript[h, i]),  …,  
      (Subscript[h, j]), …, (Subscript[h, m])⟩ :=  ⟨ -(Subscript[H, 1]), …, (Subscript[u, i]) - (Subscript[H, i]), …, - (Subscript[u, j]) - (Subscript[H, j]), …, -(Subscript[H, m])⟩

Summarizing: the S-polynomials give a handle for obtaining a finite basis for the set of all syzygies!

(The inhomogeneous equation

\(TraditionalForm\`\(\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \)\(\(h\_\(\(1\)\(\ \)\) . \ \ f\_\(\(1\)\(\ \)\) + \ \ …\ \  + \ 
        h\_m\  . \ f\_m\)\(\ \ \)\(=\)\(\ \ \)\(g\)\(\ \ \ \ \)\)\)\)

can be solved by finding one solution of the inhomogeneous equation and adding the solutions of the homogeneous equations.)

(In case { (Subscript[f, 1]),  …,  (Subscript[f, m])}  is not a Gröbner basis, transform to Gröbner basis by the extended Gröbner basis algorithm, solve,  and transform solutions back.)

(The case of several linear diophantine equations with polynomial coefficients can be reduced to the case of one equation. Alternatively, the entire Gröbner bases approach can be formulated for polynomial "modules" instead of polynomial rings.)

Application: Solving Polynomial Systems

Is based on the elimination property of Gröbner bases (w.r.t. lexicographic orderings).

A Simple System of Equations

(Subscript[f, 1])=-2 y+x y
(Subscript[f, 2])=-(x^2)+(y^2)

Find x, y such that

-2 y+x y=0
-(x^2)+(y^2)=0

We compute

G = GroebnerBasis[{(Subscript[f, 1]), (Subscript[f, 2])}, {y, x}]

Solve[-2 (x^2) + (x^3) == 0, x]

{G[[2]], G[[3]]} /. {x -> 2}

Solve[-4 + (y^2) == 0, y]

All this is already implemented in the Mathematica general Solve function:

Solve[{(Subscript[f, 1]) == 0, (Subscript[f, 2]) == 0}, {x, y}]

Theorem (BB): Solvability and the number of solutions can be predicted from the form of the Groebner basis.

A More Complicated System of Equations

(Subscript[f, 1])=x y-2  y z - z;
(Subscript[f, 2]) = (y^2) - (x^2) z  +  x z;
(Subscript[f, 3])=(z^2)-(y^2) x + x;

F  =  {(Subscript[f, 1]), (Subscript[f, 2]), (Subscript[f, 3])};

{time, G} = GroebnerBasis[F]  //  Timing

zsolexact1 = Solve[G[[1]] == 0, z]

One can compute with these "abstract roots" like with "square roots". For example

G0 = G  /.  zsolexact1[[2]] // Simplify

G0 /. {Root[-1 - 4 #(1^2) + 17 #(1^3) - 3 #(1^4) + 45 #(1^5) - 
                60 #(1^6) + 29 #(1^7) - 124 #(1^8) + 48 #(1^9) - 64 #(1^10) + 
                64 #(1^11) &, 1] -> α}

No more details in this talk!

Alternatively, compute numerically:

zsol = NSolve[G[[1]] == 0, z]

Gsubnum = G  /.  zsol[[1]]

PolynomialGCD[Gsubnum[[2]], Gsubnum[[3]]]

ysol = NSolve[ Gsubnum[[2]] == 0, y]

ysol = NSolve[ Gsubnum[[3]] == 0, y]

Theorem (Roider, Kalkbrener et al. 1990): It suffices to consider the poly in y with lowest degree.

xsol = NSolve[ Gsubnum[[4]] == 0, x]

F /. zsol[[1]] /. ysol[[1]] /. xsol[[1]]

Application: Invariant Theory

A Question:  Can

h = ((Subscript[x, 1])^7) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^7)

be expressed as a polynomial in

F = {((Subscript[x, 1])^2) + ((Subscript[x, 2])^2), ((Subscript[x, 1])^2) ((Subscript[x, 2])^2), ((Subscript[x, 1])^3) (Subscript[x, 2]) - 
          (Subscript[x, 1]) ((Subscript[x, 2])^3)}

?

Note: These polynomials are fundamental invariants for (Subscript[ℤ, 4]), i.e. a set of generators for the ring

{f ∈ ℂ[(Subscript[x, 1]), 
              (Subscript[x, 2])]  \[VerticalSeparator]  f ((Subscript[x, 1]), (Subscript[x, 2])) = 
        f (-(Subscript[x, 2]), (Subscript[x, 1]))},

i.e.

{((Subscript[x, 1])^2) + ((Subscript[x, 2])^2), ((Subscript[x, 1])^2) ((Subscript[x, 2])^2), ((Subscript[x, 1])^3) (Subscript[x, 2]) - 
          (Subscript[x, 1]) ((Subscript[x, 2])^3)} /. {(Subscript[x, 1]) -> -(Subscript[x, 2]), 
        (Subscript[x, 2]) -> (Subscript[x, 1])}

and all invariants can be expressed as polynomials in these invariants.

Reduction to Groebner Bases Computation

{time, GB} = 
      GroebnerBasis[{-(Subscript[i, 1]) + ((Subscript[x, 1])^2) + 
              ((Subscript[x, 2])^2), -(Subscript[i, 2]) + ((Subscript[x, 1])^2) 
                ((Subscript[x, 2])^2), -(Subscript[i, 3]) + ((Subscript[x, 1])^3) (Subscript[x, 2]) - 
              (Subscript[x, 1]) ((Subscript[x, 2])^3)}, {(Subscript[x, 2]), (Subscript[x, 1]), (Subscript[i, 3]), (Subscript[i, 2]), (Subscript[i, 1])}] // 
        Timing

PolynomialReduce[((Subscript[x, 1])^7) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^7), 
      GB, {(Subscript[x, 2]), (Subscript[x, 1]), (Subscript[i, 3]), (Subscript[i, 2]), (Subscript[i, 1])}, 
      MonomialOrder -> Lexicographic]

{{0, -(Subscript[i, 3]) - (1/2) (Subscript[i, 1]) (Subscript[x, 1]) (Subscript[x, 2]) - (Subscript[x, 1]^3) (Subscript[x, 2]), 
          0, ((3 (Subscript[i, 1]) (Subscript[x, 2]))/4) - (1/2) (Subscript[x, 1]^2) (Subscript[x, 2]) + ((Subscript[x, 2]^3)/2), 
          (Subscript[i, 1]) - ((Subscript[x, 1]^2)/2) + ((3 (Subscript[x, 2]^2))/4), ((3 (Subscript[i, 1]) (Subscript[x, 1]))/2) + 
            (Subscript[x, 1]) (Subscript[x, 2]^2), 
          ((Subscript[x, 2]^4)/2), -(1/4) (Subscript[i, 1]^2) (Subscript[x, 1]) (Subscript[x, 2]) - 
            (1/2) (Subscript[i, 1]) (Subscript[x, 1]) (Subscript[x, 2]^3) - (Subscript[x, 1]) (Subscript[x, 2]^5)},(Subscript[i, 1]^2) (Subscript[i, 3]) - (Subscript[i, 2]) (Subscript[i, 3])}

Theorem (Sweedler, Sturmfels et al. 1988): h can be represented in terms of I iff remainder of h w.r.t. "Groebner basis of I with slack variables" is a polynomial in the slack variables (which gives the representation).

(Subscript[i, 1]^2) (Subscript[i, 3]) - (Subscript[i, 2]) (Subscript[i, 3]) /. {(Subscript[i, 1]) -> ((Subscript[x, 1])^2) + ((Subscript[x, 2])^2), 
          (Subscript[i, 2]) -> ((Subscript[x, 1])^2) ((Subscript[x, 2])^2), 
          (Subscript[i, 3]) -> ((Subscript[x, 1])^3) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^3)}  // 
      Expand

R = 
      PolynomialReduce[((Subscript[x, 1])^6) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^6), 
        GB, {(Subscript[x, 2]), (Subscript[x, 1]), (Subscript[i, 3]), (Subscript[i, 2]), (Subscript[i, 1])}, 
        MonomialOrder -> Lexicographic]

{{0, (((Subscript[i, 1]) (Subscript[x, 1]))/2) - (Subscript[i, 1]) (Subscript[x, 2]) - (Subscript[x, 1]^2) (Subscript[x, 2]), 
          0, ((3 (Subscript[i, 1]))/4) - ((Subscript[x, 1]^2)/2) + 
            ((Subscript[x, 2]^2)/2), -((Subscript[x, 1])/4) + ((3 (Subscript[x, 2]))/4), ((3 (Subscript[i, 1]))/4) + 
            (Subscript[x, 1]) (Subscript[x, 2]), 
          ((Subscript[x, 2]^3)/2), -(1/4) (Subscript[i, 1]^2) (Subscript[x, 1]) - 
            (1/2) (Subscript[i, 1]) (Subscript[x, 1]) (Subscript[x, 2]^2) - (Subscript[x, 1]) (Subscript[x, 2]^4)},-(Subscript[i, 1]^3) (Subscript[x, 1]) + 2 (Subscript[i, 1]) (Subscript[i, 2]) (Subscript[x, 1]) + 
            (1/2) (Subscript[i, 1]) (Subscript[i, 3]) (Subscript[x, 1]) + (Subscript[i, 1]^2) (Subscript[x, 1]^3) - (Subscript[i, 2]) (Subscript[x, 1]^3) + 
            (1/2) (Subscript[i, 3]) (Subscript[x, 1]^3) + (1/2) (Subscript[i, 1]) (Subscript[i, 2]) (Subscript[x, 2])}

((Subscript[x, 1])^6) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^6) can not be expressed by the fundamental invariants in I.

((Subscript[x, 1])^6) (Subscript[x, 2]) - (Subscript[x, 1]) ((Subscript[x, 2])^6) /. {(Subscript[x, 1]) -> -(Subscript[x, 2]), 
        (Subscript[x, 2]) -> (Subscript[x, 1])}

Application: Automated (Dis-) Proving in Geometry

Reduction of the Problem to Gröbner bases computation:    

                Geo Theorem        ⟶  ( by coordinatization )
               (Underscript[∀ , x, y,   ... ])( poly1(x,y,...)=0 ∧ ... => poly(x,y,...)=0 )   ⟶
               
               ¬ (Underscript[∃ , x, y,   ... ]) (  poly1(x,y,...)=0 ∧ ... ∧ poly(x,y,...)≠0 )  ⟶
               
               ¬(Underscript[∃, x,y, ...,a])(  poly1(x,y,...)=0 ∧ ... ∧  a . poly(x,y,...) - 1 = 0 )

The latter question can be decided by the Gröbner basis method!

The method is implemented in the Theorema System:

B. B., C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. The Theorema Project: A Progress Report. In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6-7, 2000, St. Andrews, Scotland), M. Kerber and M. Kohlhase (eds.), A.K. Peters, Natick, Massachusetts, ISBN 1-56881-145-4, pp. 98-113.

Example: Pappus Theorem

What does the theorem say geometrically?

Textbook formulation:

Let A, B,  C and A1, B1,  C1 be on two lines and P = A B1 ⋂ A1 B, Q = A C1 ⋂ A1 C, S = B C1 ⋂ B1 C. Then P, Q, and S are collinear.

Input to the system:

Proposition["Pappus",  any[A, B, A1, B1, C, C1, P, Q, S], 
      point[A, B, A1, B1] ∧ pon[C, line[A, B]] ∧ 
          pon[C1, line[A1, B1]] ∧ 
          inter[P, line[A, B1], line[A1, B]] ∧ 
          inter[Q, line[A, C1], line[A1, C]] ∧ 
          inter[S, line[B, C1], line[B1, C]] \[Implies] 
        collinear[P, Q, S]]

Input to the system:

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> True}]

Notebook generated automatically by the proving algorithm based on Groebner basis algorithm:

Example: Butterfly Theorem

Textbook formulation:

A, B, C and D are four points on circle (O). E is the intersection of AC and BD. Through E draw a line perpendicular to OE, meeting AD at F and BC at G. Show that (OverBar[FE]) = (OverBar[GE]).

Remark:

Using the default coordinate system the algebraic methods are very slow.

Input to the system:

Proposition["Butterfly", any[O, A, B, C, D, EE, F, G], 
      point[O, A] ∧ 
pon[C, 
            circle[O, A]] ∧ 
pon[B, 
            circle[O, A]] ∧ 
pon[D, 
            circle[O, A]] ∧ 
inter[EE, line[A, C], 
            line[B, D]] ∧ inter[F, line[D, A], tline[EE, EE, O]] ∧ 
          inter[G, line[B, C], line[EE, F]]
 \[Implies] 
        distequal[EE, F, G, EE]]

Input to the system:

Simplify[Proposition["Butterfly"], 
      by -> GraphicSimplifier]

Output generated automatically by the system

End of output

Input to the system:

KnowledgeBase["Butterfly_g", 
      any[O, A, B, C, 
        D], {{ O, {100, 100}}, {A, {0, 100}}, {B, {55, 
            190}}, {C, {171, 170}}, {D, {60, 10}}}]

Input to the system:

Simplify[Proposition["Butterfly"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Butterfly_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Butterfly"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook

Example: The Correctness of Origami Constructions (jointly with T. Ida)

Example of an Origami Construction Problem: Starting from a square A, B, C, D, find a sequence of origami steps such that, finally, we arrive at an equilateral triangle.

A first solution (does not yield maximum edge length; other solution and more complicated examples see T. Ida, BB, J. Robu et al. 2003 and 2004):

Then we fix the point A and fold so that point D will lie on line EF. (This is a legal origami operation.)

Now we can do the analogous step with corner C, fixing B and bringing C onto the current position of D.

An Origami Proof Problem: Prove that, for all squares ABCD, \(TraditionalForm\`GD\&_\) = 2 \(TraditionalForm\`ED\&_\).

The Translation into a Prove Problem on Equalities:

First, note that \(TraditionalForm\`AB\&_\) = \(TraditionalForm\`BC\&_\) = \(TraditionalForm\`CD\&_\) = \(TraditionalForm\`DA\&_\), since we start from a square. Hence, whenever the length of one of these four edges occurs, we replace it by \(TraditionalForm\`AB\&_\).

Now observe that

\(DF\&_\^2 = \(AD\&_\^2 - AF\&_\^2 = \(AB\&_\^2 - \((AB\&_/2)\)\^2 = 
          3/4 \(\( AB\&_\^2\)\(.\)\)\)\)\)

and

\(GD\&_\^2 = \(GE\&_\^2 + 
          ED\&_\^2 = \(\((DC\&_/2 - GD\&_)\)\^2 + \((EF\&_ - DF\&_)\)\^2 = \((AB\&_/2 - GD\&_)\)\^2 + \(\(\((AB\&_ - DF\&_)\)\^2\)\(.\)\)\)\)\)

We want to decide whether, under these assumptions,

\(TraditionalForm\`GD\&_ = \(2  ED\&_ = \(2 \((EF\&_ - DF\&_)\) = 
          2 \(\((AB\&_ - DF\&_)\)\(.\)\)\)\)\)

For abbreviation, let's write

\(a = AB\&_, \ b = GD\&_, f = \(\(DF\&_\)\(.\)\)\)

Then, what we want to prove is that

(Underscript[∀ , a ≠ 0, f, b])({({{(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}})}\[Implies](b = 2 (a - f)))

The Transformation to a Groebner Basis Construction Problem:

This is equivalent to

(Underscript[(¬ ∃ ), a, f, b])({({{a ≠ 0}, {(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}, {b ≠ 2 (a - f)}})}),

which is equivalent to

(Underscript[(¬ ∃ ), a, f, b, ξ, η])({({{a η = 1}, {(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}, {(b - 2 (a - f)) ξ = 1}})}),

This question can be decided by computing the (reduced) Gröbner basis

J = 
      GroebnerBasis[{a η - 1, (f^2) - 3/4  (a^2), 
          (b^2) - (((a/2 - b))^2) - (((a - f))^2), (b - 
                  2 (a - f)) ξ - 1}, {ξ, η, b, f, 
          a}]

and to check whether or not this Gröbner basis is equal to {1}. Since this is the case, we know that the restricted version of the theorem is true.

Application: Graph Coloring

The Problem:

Find all admissible colorings in k colors of a graph with n vertices and edges E:

An admissible coloring in 3 colors of a graph with 4 vertices and edges {1,2}, {1,3}, {2,3}, {3,4}:

Not an admissible coloring in 3 colors of the same graph:

The Translation into a Groebner Bases Problem

Theorem: The possible colorings of the above graph correspond 1-1 to the common solutions of the following set of polynomials:

(((Subscript[x, 1])^2) + (Subscript[x, 1]) (Subscript[x, 2]) + ((Subscript[x, 2])^2)) ((Subscript[x, 1]) - (Subscript[x, 2])) // 
      Expand

{ -1 + 
        ((Subscript[x, 1])^3),      ...  at vertex 1 color is a 3 - 
        ary root of 1
 - 1 + 
        ((Subscript[x, 2])^3),    ...  at vertex 2 color is a 3 - 
        ary root of 1
 - 1 + 
        ((Subscript[x, 3])^3), 
-1 + 
        ((Subscript[x, 4])^3), 
((Subscript[x, 1])^2) + (Subscript[x, 1]) (Subscript[x, 2]) + 
        ((Subscript[x, 2])^2),   ... the colors at 1 and 2 must be different, 
((Subscript[x, 1])^2) + (Subscript[x, 1]) (Subscript[x, 3]) + 
        ((Subscript[x, 3])^2), 
((Subscript[x, 2])^2) + (Subscript[x, 2]) (Subscript[x, 3]) + 
        ((Subscript[x, 3])^2), 
((Subscript[x, 3])^2) + (Subscript[x, 3]) (Subscript[x, 4]) + 
        ((Subscript[x, 4])^2)}

Solution by Groebner Bases

Compute a Groebner basis of this polynomial set and compute all solutions.

GB = 
      GroebnerBasis[{-1 + (Subscript[x, 1]^3), -1 + (Subscript[x, 2]^3), -1 + 
            (Subscript[x, 3]^3), -1 + (Subscript[x, 4]^3), (Subscript[x, 1]^2) + (Subscript[x, 1]) (Subscript[x, 2]) + (Subscript[x, 2]^2), 
          (Subscript[x, 1]^2) + (Subscript[x, 1]) (Subscript[x, 3]) + (Subscript[x, 3]^2), (Subscript[x, 2]^2) + (Subscript[x, 2]) (Subscript[x, 3]) + (Subscript[x, 3]^2), 
          (Subscript[x, 3]^2) + (Subscript[x, 3]) (Subscript[x, 4]) + (Subscript[x, 4]^2)}, 
{(Subscript[x, 4]), (Subscript[x, 3]), 
          (Subscript[x, 2]), (Subscript[x, 1])}]

Solve[{-1 + (Subscript[x, 1]^3) == 0, -1 + (Subscript[x, 2]^3) == 0, -1 + (Subscript[x, 3]^3) == 
          0, -1 + (Subscript[x, 4]^3) == 0, (Subscript[x, 1]^2) + (Subscript[x, 1]) (Subscript[x, 2]) + (Subscript[x, 2]^2) == 0, 
        (Subscript[x, 1]^2) + (Subscript[x, 1]) (Subscript[x, 3]) + (Subscript[x, 3]^2) == 0, 
        (Subscript[x, 2]^2) + (Subscript[x, 2]) (Subscript[x, 3]) + (Subscript[x, 3]^2) == 0, 
        (Subscript[x, 3]^2) + (Subscript[x, 3]) (Subscript[x, 4]) + (Subscript[x, 4]^2) == 0}, 
{(Subscript[x, 4]), (Subscript[x, 3]), 
        (Subscript[x, 2]), (Subscript[x, 1])}]

Slightly re-organized output:

{{(Subscript[x, 1]) -> 1, (Subscript[x, 2]) -> -(((-1))^(1/3)), 
          (Subscript[x, 3]) -> -1 + (((-1))^(1/3)), (Subscript[x, 4]) -> 1},{(Subscript[x, 1]) -> 1,(Subscript[x, 2]) -> -(((-1))^(1/3)),(Subscript[x, 3]) -> -1 + (((-1))^(1/3)),(Subscript[x, 4]) -> -(((-1))^(1/3))},{(Subscript[x, 1]) -> 1, (Subscript[x, 2]) -> (((-1))^(2/3)), 
          (Subscript[x, 3]) -> -1 - (((-1))^(2/3)), (Subscript[x, 4]) -> 1},{(Subscript[x, 1]) -> 1, (Subscript[x, 2]) -> (((-1))^(2/3)), 
          (Subscript[x, 3]) -> -1 - (((-1))^(2/3)), 
          (Subscript[x, 4]) -> (((-1))^(2/3))},{(Subscript[x, 1]) -> -(((-1))^(1/3)), (Subscript[x, 2]) -> 1, 
          (Subscript[x, 3]) -> -1 + (((-1))^(1/3)), (Subscript[x, 4]) -> 1},{(Subscript[x, 1]) -> -(((-1))^(1/3)), (Subscript[x, 2]) -> 1, 
          (Subscript[x, 3]) -> -1 + (((-1))^(1/3)), 
          (Subscript[x, 4]) -> -(((-1))^(1/3))},{(Subscript[x, 1]) -> -(((-1))^(1/3)), 
          (Subscript[x, 2]) -> -1 + (((-1))^(1/3)), (Subscript[x, 3]) -> 1, 
          (Subscript[x, 4]) -> -(((-1))^(1/3))},{(Subscript[x, 1]) -> -(((-1))^(1/3)), 
          (Subscript[x, 2]) -> -1 + (((-1))^(1/3)), (Subscript[x, 3]) -> 1, 
          (Subscript[x, 4]) -> -1 + (((-1))^(1/3))},{(Subscript[x, 1]) -> (((-1))^(2/3)), (Subscript[x, 2]) -> 1, 
          (Subscript[x, 3]) -> -1 - (((-1))^(2/3)), (Subscript[x, 4]) -> 1},{(Subscript[x, 1]) -> (((-1))^(2/3)), (Subscript[x, 2]) -> 1, 
          (Subscript[x, 3]) -> -1 - (((-1))^(2/3)), 
          (Subscript[x, 4]) -> (((-1))^(2/3))},{(Subscript[x, 1]) -> (((-1))^(2/3)), 
          (Subscript[x, 2]) -> -1 - (((-1))^(2/3)), (Subscript[x, 3]) -> 1, 
          (Subscript[x, 4]) -> (((-1))^(2/3))},{(Subscript[x, 1]) -> (((-1))^(2/3)), 
          (Subscript[x, 2]) -> -1 - (((-1))^(2/3)), (Subscript[x, 3]) -> 1, 
          (Subscript[x, 4]) -> -1 - (((-1))^(2/3))}}

For example, {(Subscript[x, 1]) -> 1, (Subscript[x, 2]) -> -(((-1))^(1/3)), 
        (Subscript[x, 3]) -> -1 + (((-1))^(1/3)), 
        (Subscript[x, 4]) -> -(((-1))^(1/3))}corresponds to

Application: Integer Optimization

Example (B. Sturmfels):

What is the minimum number of coins (e.g. p Pennies, n Nickels, d Dimes, q Quarters) for composing a given value, e.g. 117?

Reduction to Gröbner Bases Problem (C. Traverso et al. 1986):

Code the integer values p, n, d, q as exponents of power products!

Code the goal function as the (generalized) degree of the power products!

Code the exchange rules of the coins (the relations between the quantities) as polynomials consisting of power products:

F = {(P^5) - N, (P^10) - D, (P^25) - Q}

Now compute the Gröbner basis of F (w.r.t. degree ordering):

G = 
      GroebnerBasis[F, MonomialOrder -> DegreeLexicographic]

Now you can be sure that, starting with any admissible solution (e.g. (p=17, n=10, d=5, q=0),  by reduction modulo G, you will end up with a minimal solution:

PolynomialReduce[(P^17) (N^10) (D^5), G, , 
      MonomialOrder -> DegreeLexicographic]

Answer: take 4 quarters, 1 dime, 1 nickel, 2 pennies.

Application: Symbolic Solution of Boundary Value Problems (Differential Equations)

See work by Markus Rosenkranz,  PhD thesis 2003 and RISC / RICAM Project "Scientific Computing".

Will be presented in Workshop D2.

Other Applications

Algebraic Geometry
Coding Theory   D1
Cryptography   D1
Invariant Theory
Algebraic Combinatorics  D1
Integer Optimization
Statistics
Combinatorial and Special Function Identities  D2
Symbolic Integration  D2
Symbolic Summation D2
Control Theory  D3

How Difficult is the Construction of Gröbner Bases?

Very Easy

The structure of the algorithm is easy. The operations needed in the algorithm are elementary. "Every high-school student can execute the algorithm." (See palm-top TI-98.)

Very Difficult

The inherent complexity of the problems that can be solved by the GB method (e.g. graph colorings) is "exponential". Hence, the worst-case complexity of the GB algorithm must be high.

Sometimes Easy

Mathematically interesting examples often have a lot of "structure" and, in concrete examples, GB computations can be reasonably, even surprisingly, fast.

Enormous Potential for Improvement

More mathematical theorems can lead to drastic speed-up:

The use of "criteria" for eliminating the consideration of certain S-polynomials.

p-adic approaches and floating point approaches.

The "Gröbner Walk" approach.

The "linear algebra" approach.

The "numerics" approach.

Tuning of the algorithm:

Heuristics, strategies for choosing orderings, selecting S-polynomials etc.

Good implementation techniques.

A huge literature.

Why "Gröbner" Bases?

Professor  Wolfgang Gröbner (1899-1980) was my PhD thesis supervisor.

He gave me the problem of finding "the uncovered points if the black points are given".

In my thesis (1965, will be reprinted in English in the JSC 2006) and journal publication  (1970, re-printed in BB, F. Winkler, 1998) I introduced:

* the concept of Gröbner bases and reduced Gröbner bases
* the S-polynomials
* the main theorem with proof
* the algorithm with termination and correctness proof
* the uniqueness of Gröbner bases
* first applications (computing in residue rings, Hilbert function, algebraic systems)
* the technique of base-change w.r.t. to different orderings
* a complete computer implementation 
* first complexity considerations.

Also various details of the algorithm are discussed, which later have been forgotten:

* store intermediate polynomials  
* presentation of power products by numbers
* reduction is linear algebra

(In the early days of computing, as a tendency, one tried to save memory and compensate by time.)

However, in the thesis, I did not use the name "Gröbner bases". I introduced this name only in 1976, for honoring Gröbner, when people started to become interested in my work.

My later contributions:

* the technique of criteria for eliminating unnecessary reductions
* an abstract characterization of "Gröbner bases rings", see Workshop C "Formal Gröbner Bases Theory".

More Info on Gröbner Bases?

Gröbner Bases 98 Conference:

B. B., F. Winkler. Gröbner Bases: Theory and Applications. Cambridge University Press, 1998. 560 pages.

This book contains tutorials and original papers.

This book contains also:

B. B. Introduction to Gröbner Bases, pp. 3-31.

B. B. An Algorithmic Criterion for the Solvability of Systems of Algebraic Equations, pp. 540-560. (English translation of the original paper from 1970, in which Gröbner bases were introduced.)

A continuation of this book is the special issue of the JSC  on Gröbner bases edited by Q.N. Tran and F. Winkler, 2000.

Gröbner Bases on Your Desk and in Your Palm

GB implementations are contained in all the current math software systems like Mathematica (see demo), Maple, Magma, Macsyma, Axiom, Derive, Reduce, Mupad, ...

Software systems specialized on Gröbner bases: RISA-ASIR (M. Noro, K. Yokoyama), CoCoA, Macaulay, Singular, ...

Gröbner bases are now availabe on the TI-98 (implemented in Derive).

Textbooks on Gröbner Bases

T. Kreuzer, L. Robbiano: Algorithmic Commutative Algebra I. Springer, Heidelber, 2000: Contains a list of all other, approx. 10, textbooks on GB.

W.W.Adams, P. Loustenau. Introduction to Gröbner Bases. Graduate Studies in Mathematics: Amer. Math. Soc., Providence, R.I., 1994.

T.Becker, V.Weispfenning. Gröbner Bases: A Computational Approach to Commutative Algebra. Springer, New York, 1993.

D.Cox, J.Little, D.O'Shea. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, New York, 1992.

....

M. Maruyama. Gröbner Bases and Applications. 2002.

M. Noro, K. Yokoyama. Computational Fundamentals of Gröbner Bases. University of Tokyo Press, 2003.

See papers data base and  books in the secretary's office.

Gröbner Bases on the Web

Search. E.g. in the Research Index you obtain ~ 3000 citations.

Original Publications on Gröbner Bases

See papers data base.

Approximately 1000 papers appeared meanwhile on Gröbner bases, see papers data base on the Web Site of the Special Semester.

J of Symbolic Computation, in particular, special issues.

ISSAC Conferences.

Mega Conferences.

ACA Conferences.

...

The essential  additional original ideas in the literature:

Gröbner bases can be constructed w.r.t. arbitrary "admissible" orderings (W. Trinks 1978)

Gröbner bases w.r.t. to "lexical" orderings have the elimination property (W. Trinks 1978)

Gröbner bases can be used for computing syzygies and the S-polys generate the module of syzygies (G. Zacharias 1978)

A given F, w.r.t. the infinitely many admissible orderings, has only finitely many Gröbner bases and, hence, we can construct a "universal" Gröbner bases for F (L. Robbiano, V. Weispfenning, T. Schwarz 1988)

Starting from a Gröbner bases for F for ordering (Subscript[O, 1]) one can "walk", by changing the basis only slightly, to a basis for a "nearby" ordering (Subscript[O, 2])  and so on ... until one arrives at a Gröbner bases for a desired ordering (Subscript[O, k]) (Kalkbrener, Mall 1995, Nam 2000).

Use arbitrary linear algebra algorithms for the reduction (remaindering) process: (Faugère 1997).

The numerics of Gröbner bases computation.

... numerours applications,

Research Topics

the inner structure of Groebner bases: generalized Sylvester matrices

the numerics of GB computations

axiomatic characterization of Groebner rings

generalizations (e.g. non-commutative poly-rings)

speeding up the computation

Groebner bases for particular classes of ideals (avoid computation)

the study of admissible orderings

new applications

Details see BB, Introduction to Gröbner Bases, in BB, FW 1998, pp. 1 - 31.

Equivalent definition of Gröbner bases:

F is a Gröbner basis  ⟺   (Subscript[-> , F]) has the Church-Rosser property.

f  (Subscript[-> , F]) g  ...  f reduces to g in one remaindering step using divisors from F.

-> is Church-Rosser    ⟺    (Underscript[∀ , (Subscript[g, 1]), (Subscript[g, 2])])   ( (Subscript[g, 1]) \(TraditionalForm\`\( ↔ \^*\)\)(Subscript[g, 2]) ⟹  (Subscript[g, 1])  \(TraditionalForm\`\(↓\^*\)\)   (Subscript[g, 2]) )

Main Theorem:

F is a Gröbner basis  ⟺   (Underscript[∀ , (Subscript[f, 1]), (Subscript[f, 2]) ∈ F])  remainder[ F, S–polynomial[(Subscript[f, 1]), (Subscript[f, 2])]] = 0.

Proof: "⟹": Easy.

For the direction "⟸" one can use the Newman Lemma (Newman 1942). (For the version of the algorithm with criteria one needs the generalized Newman lemma by BB.)  For Noetherian ->:

-> is Church-Rosser    ⟺    (Underscript[∀ , (Subscript[g, 1]), (Subscript[g, 2]), h])   ( (Subscript[g, 1])  ←  h -> (Subscript[g, 2]) ⟹  (Subscript[g, 1])  \(TraditionalForm\`\(↓\^*\)\)   (Subscript[g, 2]) )

The proof of this lemma uses Noetherian induction. By using Newman's lemma in the proof of the main theorem, one takes induction out of the proof and is left with the specific technicalities of polynomial reduction.

Hence, we have to consider, for arbitrary polynomials (Subscript[g, 1]), (Subscript[g, 2]), h,  the situation that

(Subscript[g, 1])  (Subscript[← , F])h (Subscript[-> , F])(Subscript[g, 2])

and we have to show that we can always find a polynomial p such that

(Subscript[g, 1])  \(\( -> \_F\)\^*\)  p  \(TraditionalForm\`\(\( ← \_F\)\^*\)\)  (Subscript[g, 2]).

By the assumption, there exist polynomials (Subscript[f, 1]) and (Subscript[f, 2])  in F such that h reduces w.r.t.  (Subscript[f, 1]) and (Subscript[f, 2]) . Let (Subscript[t, 1]) and (Subscript[t, 2]) be the power products in h on which these reductions work.

h  =   ...   +  □  (Subscript[t, 1])      +  ....     +    □  (Subscript[t, 1])    +  .....

- \(TraditionalForm\`\(\(u\_1\)\(\ \)\(f\_1\)\(\ \ \ \ \ \ \ \ \ \ \ \ \ \)\)\)            - \(TraditionalForm\`\(\(u\_2\)\(\ \)\(f\_2\)\(\ \ \ \ \ \ \ \ \ \ \ \ \ \)\)\)

yields (Subscript[g, 1])                    yields (Subscript[g, 2])

Cases \(TraditionalForm\`\(\(t\_1\)\(\ \)\(≺\)\(\ \)\(t\_2\)\(\ \)\)\)and \(TraditionalForm\`\(\(t\_2\)\(\ \)\(≺\)\(\ \)\(t\_1\)\(\ \)\)\) easy (but not trivial!): by "semi-compatibility" of polynomial reduction.

Cases t:= (Subscript[t, 1]) = (Subscript[t, 2]) :

h  =   ...  +   □  t     +  .....

- \(TraditionalForm\`\(\(u\_1\)\(\ \)\(f\_1\)\(\ \ \ \ \ \ \ \ \ \ \ \ \ \)\)\)  - \(TraditionalForm\`\(\(u\_2\)\(\ \)\(f\_2\)\(\ \ \ \ \ \ \ \ \ \ \ \ \ \)\)\)

In this case t is a multiple of the LCM m of LPP[(Subscript[f, 1])] and LPP[(Subscript[f, 2])]:  t = v . m.

Since, by assumption of the theorem,  the S-polynomial of (Subscript[f, 1]) and (Subscript[f, 2])  can be reduced to 0, the reduction of m in the two essentially different ways (starting once by using (Subscript[f, 1]) and once by using (Subscript[f, 2])) has a common successor.

Hence, by "stability" of  polynomial reduction, by multiplication of all the steps by v,  (Subscript[g, 1])and (Subscript[g, 2])have a common successor.

For example: How can one invent (and verify) notions like "S-polynomial", theorems like the main theorem, and algorithms like the Gröbner bases algorithm automatically, i.e. by algorithms that work on formulae.

For example, algorithm synthesis:

Given the specification  P of a problem.

Find an algorithm A such that  (Underscript[∀ , F]) P[ F, A[F]].

I succeeded to come up with a method which, for many P, yields A automatically. In particular, with this method, starting from the specification of the Gröbner bases construction problem:

           Given:  F.
           Find:    G  such that   
                                  G is finite
                                  G is a Gröbner basis
                                  Ideal[F] = Ideal[G],

one arrives automatically at the notion of S-polynomials and the above Gröbner bases algorithm based on the notion of S-polynomials.

For details see the recent publication

B. Buchberger
Towards the Automated Synthesis of a Gröbner Bases Algorithm
RACSAM, 98/1 (Rev. Acad. Cienc., Spanish Royal Academy of Science), 98/1, pp. 65-75, 2005.

and the Workshop C "Formal Gröbner Bases Theory", March 6-10, in the course of this special semester,