Symbolic Computation:
Current Trends

Bruno Buchberger

Talk at ACAT05 (Algorithmic Information Theory)
DESY, Zeuthen, Germany, May 26, 2005

RISC (Research Institute for Symbolic Computation)
Johannes Kepler University

RICAM (Radon Institute for Computational and Applied Mathematics)
Austrian Academy of Science

Linz, Austria

Copyright: Bruno Buchberger 2005
Copying, Printing and Storing of this file is granted under the following conditions:
- the file is kept unchanged (including this copyrigh note)
- a message is sent to bruno.buchberger@jku.at
- if you use material presented in this talk, cite the talk appropriately.

The Evolution of "Computing"

The Evolution of "Computing"

In This Talk

All Current Algorithmics (Numerics, Symbolics,...) is Available in Systems

Systems like Mathematica, Maple, Derive, Mathlab, ... FORM, Singular, Cocoa, ...

An enormous potential for science (physics, ...) and engineering.

Help!

Example:

DSolve[{y''[x] == a  y'[x] + y[x], 
        y[0] == 1, y'[0] == 0}, y, x]

Example:

Solve[{(1/s) + (1/t) == (1/F), (1/(d + s)) + (1/(t - e)) == (1/F), 
        c == ((e F)/(f (t - e))), M == (t/s)}, {d, e, s, 
        t}]

Remark:

There is lots of new and deep mathematics behind the (numeric, discrete, graphic, algebraic, and symbolic) algorithms of the current math systems.

In this talk only one example: Gröbner bases theory:

What are Gröbner bases?

How can Gröbner bases be computed?

Why are Gröbner bases important? (Dozens of fundamental problems can be reduced to Gröbner bases construction!)

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 ...)

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

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.

for all (Subscript[f, 1]),...,(Subscript[f, m])∈ F and all (infinitely many) 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.

The "Main Theorem" of 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.

S–polynomial[-2 y+x y,-(x^2)+(y^2)]=y  (-2 y+x y)-x  (-(x^2)+(y^2))

Proof: Nontrivial. Combinatorial.

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 all (infinitely many) 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.

The Problem of Constructing Gröbner Bases

Given F,  find G   such that G is a Gröbner basis 
                                            and F and G generate the same set of linear combinations.

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.

Termination of the Algorithm

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

Example of Application: Solve Systems

(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

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

Gsubnum = G  /.  zsol[[1]]

ysol = NSolve[ Gsubnum[[2]] == 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]]

Example of 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 the group (Subscript[ℤ, 4]).

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]

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]

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

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:

{ -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.

More Applications

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.

Example: The Numerics of Gröbner Bases

In both directions (H. Stetter 1987 - 2005):

Start from Gröbner bases and compute solutions (reduction to an eigenvalue problem).

Numerically, compute (a numerical variant) of Gröbner bases.

Example: Computation on Operators

computation on (finitary representations of) numbers: e.g. computation on algebraic numbers

↓

computation on (finitary representations of) functions (on numbers): e.g. symbolic integration

↓

computation on (finitary representations of) operators (on functions): e.g. symbolic generation of Green's funtions for boundary-value problems

Project SFB 1322  (B.B. and H. Engl, RICAM), PhD thesis and postdoc work of M. Rosenkranz:

M.Rosenkranz, B.B, H.W.Engl. Solving Linear BVPs via Non–commutative Gröbner Bases. Applicable Analysis, 82(7), July 2003, pp. 655–675.

M.Rosenkranz. A New Symbolic Method for Solving Linear Two–Point BVPs on the Operator Level. Journal of Symbolic Computation, 39, February 2005, pp.171–199.

Basic Idea and Procedure

FGiven a two–point BVP (e.g. beam equation):

Example: Beam Deflection

Problem:

Assuming regularity, every linear two–point BVP admits to write the solution as:

g	...................... Green's function (([a, b])^2) -> ℂ
	f	...................... Given forcing function [a, b] -> ℂ
	u	...................... Desired solution function [a, b] -> ℂ

Traditional solution method (see Kamke): Matrix inversion based on a fundamental system.

In the beam example:

We want to find its Green's operator in the sense of

We do the following:

Compute the solution space N of the homogeneous equation Tu = 0.

Determine a projector P onto N such that M = (1 - P) (C^∞)[a, b] fulfills the boundary conditions.

Find the right inverse (T^◆) of T (a variant of Moore-Penrose inverse).

Build up G = (1 - P) (T^◆) as the crude Green's operator.

Reduce G with respect to the Green's system (a non-commutative Gröbner basis by the main theorem; 233 S-polys needed!) for obtaining a standard representation.

(Optionally, extract Green's function g from standard representation of G).

The Green's System

System["1. Equalities for Isolating Differential Operators",any[f],
({{D A = 1, "DA"}, {D B = -1, "DB"}, {D ⌈f⌉ = ⌈f⌉ D + ⌈f'⌉, "DM"}, {D L = 0, "DL"}, {D R = 0, "DR"}})
]

System["2. Equalities for Isolating Boundary Operators",any[f],
({{L A = 0, "LA"}, {R A = A + B, "RA"}, {L B = A + B, "LB"}, {R B = 0, "RB"}, {L ⌈f⌉ = (f^←) L, "LM"}, {R ⌈f⌉ = (f^→) R, "RM"}, {L L = L, "LL"}, {L R = R, "LR"}, {R L = L, "RL"}, {R R = R, "RR"}})
]

System["Equalities for Algebraic Simplication",any[f, g],
({{⌈f⌉ ⌈g⌉ = ⌈f g⌉, "MM"}})
]

System["3. Equalities for Contracting Integration Operators",any[f],
({{\(A\ ⌈f⌉\ A = ⌈\(∫\^*\)f⌉ A - 
                  A\ ⌈\(∫\^*\)f⌉\), "AMA"}, {\(A\ ⌈f⌉\ B = ⌈\(∫\^*\)f⌉ B + 
                  A\ ⌈\(∫\^*\)f⌉\), "AMB"}, {\(B\ ⌈f⌉\ A = ⌈\(∫\_*\)f⌉ A + 
                  B\ ⌈\(∫\_*\)f⌉\), "BMA"}, {\(B\ ⌈f⌉\ B = ⌈\(∫\_*\)f⌉ B - 
                  B\ ⌈\(∫\_*\)f⌉\), "BMB"}, {\(A\ A = ⌈\(∫\^*\)1⌉\ A - 
                  A\ ⌈\(∫\^*\)1⌉\), "AA"}, {\(A\ B = ⌈\(∫\^*\)1⌉\ B + 
                  A\ ⌈\(∫\^*\)1⌉\), "AB"}, {\(B\ A = ⌈\(∫\_*\)1⌉ A + 
                  B\ ⌈\(∫\_*\)1⌉\), "BA"}, {\(B\ B = ⌈\(∫\_*\)1⌉ B - 
                  B\ ⌈\(∫\_*\)1⌉\), "BB"}})
]

System["4. Equalities for Absorbing Integration Operators",any[f],
({{A ⌈f⌉ D = -(f^←) 
                    L + ⌈f⌉ - 
                  A ⌈f'⌉, "AMD"}, {B ⌈f⌉ D = (f^→) 
                    R - ⌈f⌉ - 
                  B ⌈f'⌉, "BMD"}, {A D = -L + 1, "AD"}, {B D = R - 1, "BD"}, {\(A ⌈f⌉ 
                  L = ⌈\(∫\^*\)f⌉ L\), "AML"}, {\(B ⌈f⌉ 
                  L = ⌈\(∫\_*\)f⌉ L\), "BML"}, {\(A ⌈f⌉ 
                  R = ⌈\(∫\^*\)f⌉ R\), "AMR"}, {\(B ⌈f⌉ 
                  R = ⌈\(∫\_*\)f⌉ R\), "BMR"}, {\(A\ L = ⌈\(∫\^*\)1⌉\ L\), "AL"}, {\(B\ L = ⌈\(∫\_*\)1⌉\ L\), "BL"}, {\(A\ R = ⌈\(∫\^*\)1⌉\ R\), "AR"}, {\(B\ R = ⌈\(∫\_*\)1⌉\ R\), "BR"}})
]

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!

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:

Automated Proofs of Theorems in Analysis (The "PCS" Prover: BB 2001)

Initialize Theorema

Needs["Theorema`"];

Needs["Theorema`Provers`UserProvers`PCS`"]

Needs["Theorema`Provers`UserProvers`VariousPC`"]

SetGlobals[TraceLevel -> 0, DebugLevel -> 0, 
      SearchDepth -> 100, Prover -> PCS, 
      FormatMetas -> "Subscripted"]

SetOptions[Prove, transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> Proved}];

$RecursionLimit = 1024;

$TmaSolveLevel = 3;

$NDDebug = False;

Off[General::spell]

Off[General::spell1]

SetGlobals[LabelStyle -> "Numeric", 
        Prover -> NNEqIndProver];
Needs["Theorema`Provers`Cascade`Cascade`"]; 
    Needs["Theorema`Provers`Cascade`ConjectureGenerator`"]

\(Needs["Theorema`Provers`UserProvers`GroebnerBasesProver`"]; $TmaProofPresentation\  = \ 100;\)

Theorema`Provers`PCS`Solver`Private`$TmaSolveLevel=3

SetOptions[Prove, transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> 
              Proved}] ;

    $RecursionLimit = 1024;  Off[General::spell]; 
    Off[General::spell1]; $TmaQRTarget = {"kb", "goal"};

Example

Definition[\("limit:", any[f, a], 
	
      limit[f, a]⟺\ \(\(∀ \+ϵ\)\+\(ϵ > 0\)\(∃ \+N\(\(∀ \+n\)\+\(n ≥ N\)\[LeftBracketingBar]f[n] - 
                    a\[RightBracketingBar] < ϵ\)\)\)\)]

Proposition[\("limit of sum", 
      any[f, a, g, 
        b], 
	\((limit[f, a] ∧ 
            limit[g, b])\)\ \ \ \ \  \[Implies] \ \ \ \ \ limit[f + g, 
          a + b]\)]

Definition[\("+:", 
      any[f, g, x], 
	\((f + g)\)[x] = f[x] + g[x]\)]

Lemma[\("|+|", 
      any[x, y, a, 
        b, δ, ϵ], 
	\((\[LeftBracketingBar]\((x + 
                    y)\) - \((a + 
                    b)\)\[RightBracketingBar] < \((δ + ϵ)\))\)\ \ \ \ ⟸\ \ \ \((\[LeftBracketingBar]x - a\[RightBracketingBar] < δ ∧ \[LeftBracketingBar]y - 
                  b\[RightBracketingBar] < ϵ)\)\)]

Lemma[\("max", any[m, M1, M2], 
	
      m ≥ 
          max[M1, M2]\ \ \ \ \  \[Implies] \ \ \ \ \ \((m ≥ 
              M1 ∧ m ≥ M2)\)\)]

Theory["limit",
	({{Definition["limit:"]}, {Definition["+:"]}, {Lemma["|+|"]}, {Lemma["max"]}})]

Prove[Proposition["limit of sum"], 
      using -> Theory["limit"], by -> PCS]

Proof contains interesting algorithmic and didactic information!

Algorithm-Supported Mathematical Theory Exploration

A new world-wide movement (approx. 20 research groups, e.g. Mizar, Isabelle, Omega, NuPrL, Coq, etc.)

Our Theorema Group is a (founding) member of this network.

Goals:

invent (axioms, definitions for) new concepts (operations: predicates, functions)   (e.g. limit)

invent and prove properties of notions

invent problems about notions

invent methods (algorithms) for problems and prove their correctness

compute (apply algorithms to data)

organize, store, and retrieve knowledge

Example: Automated Synthesis of the Gröbner Bases Algorithm (BB 2005)

Starting from a formal (predicate logic) specification of the problem,

by this new algorithm synthesis method,

the key idea of the main theorem (the notion of S-polynomial) is automatically generated and verified.

Conclusions

Intellectics:

= algorithm-supporte mathematical theory exploration

= mathematical knowledge management

= "(Anti)bourbakism of the 21st century"

Will drastically change the way

- how we do research in math,
- how we teach math,
- how we apply math,
- how we store and retrieve math knowledge.

For Physics ?

Special Semester on Gröbner Bases, Feb - July 2006

At RICAM and RISC, see       
           www.ricam.ac.at
goto "expression of interest" form: visiting researcher, postdoc, and doc fellowships available.

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. (Generalized Sylvester matrices.)

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) and journal publication  (1970) 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.

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".

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.

Gröbner Bases on the Web

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

Original Publications on Gröbner Bases

Approximately 600 papers appeared meanwhile on Gröbner bases.

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).

... 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

applications (problem reductions, e.g. functional analysis, BV problems, Rosenkranz 2003)

References

On Gröbner Bases

[Buchberger 1970]
B. Buchberger. Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems (An Algorithmical Criterion for the Solvability of Algebraic Systems of Equations). Aequationes mathematicae 4/3, 1970, pp. 374-383. (English translation in: [Buchberger, Winkler 1998],  pp. 535 -545.) Published version of the PhD Thesis of B. Buchberger, University of Innsbruck, Austria, 1965.

[Buchberger 1998]
B. Buchberger. Introduction to Gröbner Bases. In: [Buchberger, Winkler 1998], pp.3-31.

[Buchberger, Winkler, 1998]
B. Buchberger, F. Winkler (eds.). Gröbner Bases and Applications, Proceedings of the International Conference "33 Years of Gröbner Bases", 1998, RISC, Austria, London Mathematical Society Lecture Note Series, Vol. 251, Cambridge University Press, 1998.

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

On Mathematical Knowledge Management

B. Buchberger, G. Gonnet, M. Hazewinkel (eds.)
Mathematical Knowledge Management.
Special Issue of Annals of Mathematics and Artificial Intelligence, Vol. 38, No. 1-3, May 2003, Kluwer Academic Publisher, 232 pages.

A.Asperti, B. Buchberger, J.H.Davenport (eds.)
Mathematical Knowledge Management.
Proceedings of the Second International Conference on Mathematical Knowledge Management (MKM 2003), Bertinoro, Italy, Feb.16-18, 2003, Lecture Notes in Computer Science, Vol. 2594, Springer, Berlin-Heidelberg-NewYork, 2003, 223 pages.

A.Asperti, G.Bancerek, A.Trybulec (eds.).
Proceedings of the Third International Conference on Mathematical Knowledge Management, MKM 2004,
Bialowieza, Poland, September 19-21, 2004,  Lecture Notes in Computer Science, Vol. 3119, Springer, Berlin-Heidelberg-NewYork, 2004

On Theorema

[Buchberger et al. 2000]
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. The Theorema Project: A Progress Report. In: M. Kerber and M. Kohlhase (eds.), 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),  A.K. Peters, Natick, Massachusetts, ISBN 1-56881-145-4, pp. 98-113.

On Theory Exploration and Algorithm Synthesis

[Buchberger 2000] 
B. Buchberger. Theory Exploration with Theorema. 
Analele Universitatii Din Timisoara, Ser. Matematica-Informatica, Vol. XXXVIII, Fasc.2, 2000, (Proceedings of SYNASC 2000, 2nd International Workshop on Symbolic and Numeric Algorithms in Scientific Computing, Oct. 4-6, 2000, Timisoara, Rumania, T. Jebelean, V. Negru, A. Popovici eds.), ISSN 1124-970X, pp. 9-32.

[Buchberger 2003] 
B. Buchberger. Algorithm Invention and Verification by Lazy Thinking.
In: D. Petcu, V. Negru, D. Zaharie, T. Jebelean (eds), Proceedings of SYNASC 2003 (Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, October 1–4, 2003), Mirton Publishing, ISBN 973–661–104–3, pp. 2–26.

[Buchberger, Craciun 2003]
B. Buchberger, A. Craciun. Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema. in: Fairouz Kamareddine (ed.),  Proc. of the Mathematical Knowledge Management Workshop, Edinburgh, Nov. 25, 2003, Electronic Notes on Theoretical Computer Science,  volume dedicated to the MKM 03 Symposium, Elsevier, ISBN 044451290X, to appear.

[Buchberger 2004]
B. Buchberger. 
Towards the Automated Synthesis of a Gröbner Bases Algorithm.
RACSAM (Review of the Royal Spanish Academy of Science), Vol. 98/1, to appear, 10 pages.