Automated Synthesis of
a Gröbner Bases Algorithm

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

Talk at Workshop "Formal Gröbner Bases Theory"
RICAM - RISC, Linz, Austria
March 6, 2006

Copyright Note: Copyright Bruno Buchberger 2006
This file may be copied and stored in data bases under the following conditions:

-  The file is kept unchanged (including this copyright note).
-  A message is sent to Bruno.Buchberger@jku.at.
- If you use material contained in this file, cite it appropriately referring to the above talk and workshop.

Objectives

Demonstrate that

automated synthesis of non-trivial algorithms is possible,

main idea (S-polynomials) of algorithmic Gröbner bases theory can be "invented" automatically.

The algorithm synthesis method described here  can be implemented in any reasoning system that provides:

access to the proof objects even in the case of failing proofs,

a "natural" proof style (temporary assumptions and temporary goals).

An "Algorithm" for Algorithm Synthesis

Synthesis of a Gröbner Bases Algorithm

Conclusion

An "Algorithm" for Algorithm Synthesis

Synthesis of a Gröbner Bases Algorithm

Conclusion

The Algorithm Invention ("Synthesis") Problem

Given a problem specification P (in predicate logic), find an algorithm A such that

(Underscript[∀ , x]) P[x, A[x]].

Examples of specifications P:

P[x, y]  ⇔  is–greater[x, y]
P[x, y]  ⇔  
      is–sorted–version[x, y]
P[x, y]  ⇔  
      has–derivative[x, y]
P[x, y]  ⇔  
      are–factors–of[x, y]
P[x, y]  ⇔  
      is–Gröbner–basis[x, 
        y]
....

A general algorithm S for "all" P cannot exist but ...

Literature

There is a rich literature on algorithm synthesis methods, see survey

[Basin et al. 2004] D. Basin, Y. Deville, P. Flener, A. Hamfelt, J. F. Nilsson.  Synthesis of Programs in Computational Logic. In: M. Bruynooghe, K. K. Lau (eds.), Program Development in Computational Logic, Lecture Notes in Computer Science, Vol. 3049, Springer, 2004, pp. 30-65.

Our method is in the class of "scheme-based" methods. Closest (but essentially different):

[Lau et al. 1999] K. K. Lau, M. Ornaghi, S. Tärnlund. Steadfast logic programs. Journal of Logic Programming, 38/3, 1999, pp. 259-294. (Synthesis from successful proofs.)

Work in the Group of A. Bundy, Critics. (Synthesis of the appropriate induction scheme.)

The "Lazy Thinking" Method for Algorithm Synthesis (BB 2001): Intuition

"Lazy Thinking" Method for Algorithm Synthesis = My Advice to "Students" (= "Computers") How to Invent Algorithms

Given: A problem P.

Find: An algorithm A for P.

Completely understand the problem.  ("Specification" of the problem.)

Learn how to prove.

Collect (prove) "complete" knowledge on the auxiliary notion appearing in the problem.

Consider known fundamental ideas of how to structure algorithms in terms of subalgorithms ("algorithm schemes"). 
Try one scheme A after the other.

Try to prove that A solves P: From the failing proof construct specifications of the subalgorithms that make the proof successful.

The "Lazy Thinking" Method for Algorithm Synthesis: Sketch

Given a problem specification P

consider various "algorithm schemes" for A, e.g.      A[⟨⟩]=c
(Underscript[∀ , x]) A[⟨x⟩]=s[⟨x⟩]
\(∀ \+\(x, y\&_\)\)(\(A[⟨x, y, z\&_⟩]\)=i[\(x, y, 
                A[⟨y, z\&_⟩]\)])

and try to prove (automatically) (Underscript[∀ , x]) P[x, A[x]].

This proof will normally fail because nothing is known on the unspecified sub-algorithms c, s, i, ... in the algorithm scheme.

From the temporary assumptions and goals in the failing proof situation (automatically) generate such specifications for the unspecified sub-algorithms c, s, i, ... that make the proof successful.

Now, apply the method recursively to the auxiliary functions.

This synthesis method reduces the problem of finding an algorithm that satisfies the specification to finding algorithms for (automatically generated) other specifications (that are hopefully easier to satisfy or for which algorithms are already known).

Example: Synthesis of Merge-Sort [BB et al. 2003]

Problem: Synthesize "sorted" such that

(Underscript[∀ , x]) is–sorted–version[x, 
          sorted[x]].

("Correctness Theorem")

Knowledge on Problem:

(Underscript[∀ , x, y])(is–sorted–version[x, y]⇔({{is–sorted[y]}, {is–permuted–version[x, y]}}))

is–sorted[⟨⟩]

(Underscript[∀ , x]) 
        is–sorted[⟨x⟩]

\(∀ \+\(x, y, z\&_\)\)(\(is–sorted[⟨x, y, 
              z\&_⟩]\)⇔({{x ≥ y}, {\(is–sorted[⟨y, 
                    z\&_⟩]\)}}))

etc.

An Algorithm Scheme: Divide and Conquer

(Underscript[∀ , x])(A[x]={({{s[x], ⇐, is–trivial–tuple[x]}, {m[A[l[x]],A[r[x]]], ⇐, otherwise}})})

s, m, l, r  are unknowns.

We Now Start Proving the Correctness Theorem and Analyze the Failing Proof: see notebooks with failing proofs.

Automated Invention of Sufficient Specifications for the Subalgorithms

A simple (but amazingly powerful) rule    ( m  ... an unknown subalgorithm ):

Collect temporary assumptions  T[ x0, ... A [  ],  ...  ]
and temporary goals G[ x0, ...m  [  A [  ]  ]  ]

and produces specification

(Underscript[∀ , X,   ... ,  Y,   ... ])  (T[X,...Y,...]    ⟹   G[Y,...m  [Y] ] ).

Details: see papers [BB 2003] and example.

The Result of Applying Lazy Thinking in the Sorting Example

Lazy Thinking, automatically (in approx. 2 minutes on a laptop using the Theorema system), finds the following specifications for the sub-algorithms that provenly guarantee the correctness of the above algorithm (scheme):

(Underscript[∀ , x])(is–trivial–tuple[x]\[Implies]s[x]=x)

(Underscript[∀ , y, z])(({{is–sorted[y]}, {is–sorted[z]}}) \[Implies]({{is–sorted[m[y, z]]}, {m[y, z] ≈ (y ≍ z)}}) )

(Underscript[∀ , x])(l[x]≍r[x] ≈  x)

Note: the specifications generated are not only sufficient but natural !

The four proof notebooks generated automatically by Theorema that develop these specifications successively, are given in the appendix.

What Do We Have Now?

Case A: We find algorithms S, M, L, R in our knowledge base for which the properties specified above for s, m, l, r are already contained in the knowledge base or can be derived (proved) from the knowledge base.
In this case, we are done, i.e. we have synthesized a sorting algorithm.

Case B: We do not find such algorithms S, M, L, R   in our knowledge base.
In this case, we apply Lazy Thinking again in order to synthesize appropriate s, m, l, r

until we arrive at sub-sub-...-algorithms in our knowledge base (e.g. the basic operations of tuple theory like append, prepend etc.)

Case B can be avoided, if we proceed systematically bottom-up ("complete theory exploration" in layers).

Example: Synthesis of Insertion-Sort

Synthesize A such that

(Underscript[∀ , x]) is–sorted–version[x, 
          A[x]].

Algorithm Scheme: "simple recursion"

A[⟨⟩]=c
(Underscript[∀ , x]) A[⟨x⟩]=s[⟨x⟩]
\(∀ \+\(x, y\&_\)\)(\(A[⟨x, y\&_⟩]\)=i[\(x, 
            A[⟨y\&_⟩]\)])

Lazy Thinking, automatically (in approx. 2 minutes on a laptop using the Theorema system), finds the following specifications for the auxiliary functions

c=⟨⟩
(Underscript[∀ , x])(s[⟨x⟩]=⟨x⟩)
\(∀ \+\(x, y\&_\)\)(\(is–sorted[⟨y\&_⟩]\) \[Implies]({{is–sorted[i[\(x, ⟨y\&_⟩\)]]}, {i[\(⟨x, y\&_⟩\)] ≈ \((x⌣⟨y\&_⟩)\)}}) )

How Far Can We Go With the Method ?

Can we automatically synthesize algorithms for non-trivial problems?  What is "non-trivial"?

Example of a non-trivial problem: construction of Gröbner bases.

The Problem of Constructing Gröbner Bases is Non-trivial

Dozens of fundamental problems in algebraic geometry, invariant theory, optimization, graph theory, coding theory, cryptography, statistics, symbolic summation, symbolic solution of differential equations, ... can be reduced to the construction of Gröbner bases. (Approx. 1000 papers on the application of the Gröbner bases method, see B. Buchberger, A. Zapletal,  Papers Data Base on Gröbner Bases Theory, 2006, www.ricam.oeaw.ac.at/Groebner-Bases-Bibliography/index.php. )

Some of these problems were open for decades.

Main algorithmic idea of Gröbner bases theory:  The "S-polynomials"  together with the S-polynomial theorem.

[ Buchberger 1965] and [ Buchberger 1970].

Hence, question: Can Lazy Thinking automatically invent the notion of S-polynomial and automatically deliver the  algorithm based on it together with its correctness proof?

The S-Polynomials

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

x z(x y-2  y z - z-1)+y ((y^2) - (x^2) z  +  x z + 2)//Expand

S–polynomial[g1, g2]= 
form the 

least–common–multiple[leading–power–product[g1],leading–power–product[g2]]

  and then  ...

Algorithm-Supported Mathematical Theory Exploration

An "Algorithm" for Algorithm Synthesis

Synthesis of a Gröbner Bases Algorithm

Conclusion

The Problem of Constructing Gröbner Bases

Find algorithm Gb such that

(Underscript[∀ , is–finite[F]])    (({{is–finite[ Gb[F] ]}, {is–Gröbner–basis[ Gb[F]]}, {ideal[F]=ideal[ Gb[F]].}}))

Definitions [BB 1965]  :

is–Gröbner–basis[G]⇔is–confluent[ (Subscript[-> , G])].

(Subscript[-> , G])  ...  a division step.

Confluence of Division  (Subscript[-> , G])

is–confluent[->] :\(\(⇔\)\(∀ \+\(f1, f2\)\((f1\( ↔ \^*\)f2 \[Implies] 
              f1\(↓\^*\)f2)\)\)\)

Knowledge on the Concepts Involved

h1 (Subscript[-> , G])h2   \[Implies]  
          p  .  h1 (Subscript[-> , G])p  .  h2

etc.

Algorithm Scheme "Critical Pair / Completion"

({{A[F] =A[F, pairs[F]]}, {A[F, ⟨⟩]=F
}, {A[\(F, ⟨⟨g1, 
                  g2⟩, p\&_⟩\)]=
where[f=lc[g1, g2],h1 = trd[rd[f, g1], F],h2 = trd[rd[f, g2], F],
{({{A[\(F, ⟨p\&_⟩\)], ⇐, h1 = h2}, {A[F⌢df[h1, 
                                h2],\(⟨p\&_⟩\)≍⟨⟨(Subscript[F, k]),df[h1, h2]⟩ (Underscript[\[VerticalSeparator] , k = 
                                        1, …, \[LeftBracketingBar]F\[RightBracketingBar]])⟩], ⇐, otherwise}})} ]}})

This scheme can be tried in any domain, in which we have a reduction operation rd that depends on sets F of objects and a Noetherian relation ≻ which interacts with rd in the following natural way:

(Underscript[∀ , f, g])(f ⪰ 
            rd[f, g]).

The Essential Problem

The problem of synthesizing a Gröbner bases algorithm can now be also stated by asking whether, starting with the proof of

(Underscript[∀ , F])    (({{is–finite[ A[F] ]}, {is–Gröbner–basis[ A[F]]}, {ideal[F]=ideal[ A[F]]}})),

we can automatically produce the idea that

lc[g1, g2]=lcm[lp[g1], lp[g2]]

and

df[h1, h2]=h1-h2

and prove that the idea is correct.

Now Start the (Automated) Correctness Proof

With current theorem proving technology, in the Theorema system (and other provers), the proof attempt could be done automatically. (Ongoing PhD thesis of A. Craciun.)

Details

It should be clear that, if the algorithm terminates, the final result is a finite set (of polynomials) G that has the property

(Underscript[∀ , g1, g2 ∈ G])(where[f = lc[g1, g2],h1 = trd[rd[f, g1], G],h2 = trd[rd[f, g2], G],∨{({{h1 = h2}, {df[h1, h2] ∈ G}})} ]).

We now try to prove that, if G has this property, then

is–finite[G], 
ideal[F] = 
      ideal[G], 
is–Gröbner–basis[
      G],  
      i . e .  
      is–Church–Rosser[ (Subscript[-> , G])] .

Here, we only deal with the third, most important, property.

Using Available Knowledge

Using Newman's lemma and some elementary properties it can be shown that it is sufficient to prove

is–Church–Rosser[ (Subscript[-> , G])]⇔ (Underscript[∀ , p])(Underscript[∀ , f1, f2])(({({{p (Subscript[-> , G])f1}, {p (Subscript[-> , G])f2}})} )\[Implies]\(f1\(\(↓\_G\)\^*\)f2\)).

The (Automated) Proof Attempt

Let now the power product p and the polynomials f1, f2 be arbitary but fixed and assume

{({{p (Subscript[-> , G])f1}, {p (Subscript[-> , G])f2.}})}

We have to find a polyonomial g such that

({{\(\(f1\(\( -> \_G\)\^*\)g\)\(,\)\)}, {\(f2\(\( -> \_G\)\^*\)\(\(g\)\(.\)\)\)}})

From the assumption we know that there exist polynomials g1 and g2 in G such that

({{lp[g1] | p,}, {f1 = rd[p, g1],}})
({{lp[g2] | p,}, {f2 = rd[p, g2].}})

From the final situation in the algorithm scheme we know that for these g1 and g2

∨{({{h1 = h2}, {df[h1, h2] ∈ G,}})}

where

({{h1 := trd[f1', G], f1' := rd[lc[g1, g2], g1], }, {h2 := trd[f2', G], f2' := rd[lc[g1, g2], g2].}})

Case h1=h2

\(lc[g1, 
          g2]\( -> \_g1\)\(rd[lc[g1, g2], g1]\(\( -> \_G\)\^*\)trd[
            rd[lc[g1, g2], g1], G]\) = 
trd[
          rd[lc[g1, g2], g2], G]\(\( ← \_G\)\^*\)rd[lc[g1, g2], 
          g2]\( ← \_g2\)\(\(lc[g1, g2]\)\(.\)\)\)

(Note that here we used the requirements rd[lc[g1,g2],g1]≺lc[g1,g2] and rd[lc[g1,g2],g2]≺lc[g1,g2].)

Hence, by elementary properties of polynomial reduction,

\(∀ \+\(a, q\)\(\((\ 
          a\ q\ lc[g1, 
                  g2]\( -> \_g1\)\(a\ q\ rd[lc[g1, g2], 
                    g1]\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
                    G]\) = 
a\ q\ trd[rd[lc[g1, g2], g2], 
                  G]\(\( ← \_G\)\^*\)a\ q\ rd[lc[g1, g2], 
                  g2]\( ← \_g2\)\ 
              a\ q\ lc[g1, g2]\ )\)\(.\)\)\)

Now we are stuck in the proof.

Now Use the Specification Generation Algorithm

Using the above specification generation rule, we see that we could proceed successfully with the proof if lc[g1,g2] satisfied the following requirement

({{(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies]((Underscript[∃ , a, q])(p = a q lc[g1, g2] ))), , (lc requirement)}})

With such an lc, we then would have

\(p\( -> \_g1\)rd[p, 
            g1] = \(a\ q\ rd[lc[g1, g2], g1]\(\( -> \_G\)\^*\)a\ q\ trd[
                rd[lc[g1, g2], g1], 
                G] = \(a\ q\ trd[rd[lc[g1, g2], g2], 
                  G]\(\( ← \_G\)\^*\)a\ q\ rd[lc[g1, g2], g2] = 
            rd[p, g2]\( ← \_g2\)p\)\)\)}

and, hence,

\(\(\(f1\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
          G]\)\(,\)\)\)

\(\(\(f2\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
          G]\)\(,\)\)\)

i.e. we would have found a suitable g.

Summarize the (Automatically Generated) Specifications of the Subalgorithm lc

(lc requirement), which also could be written in the form:

(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies](lc[g1, g2]|p)) ,

and

({{lp[g1]|lc[g1, g2],}, {lp[g2]|lc[g1, g2],}})

wich is a consequence of

lc[g1, g2] (Subscript[-> , g1])rd[lc[g1, g2], g1], 
lc[
        g1, g2] (Subscript[-> , g2])rd[lc[g1, g2], 
          g2].

Summarize Again

For synthesizing an algorithm for the Gröbner bases problem it suffices to find an lc satisfying

(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies](lc[g1, g2]|p)) ,

and

({{lp[g1]|lc[g1, g2],}, {lp[g2]|lc[g1, g2].}})

This problem can be solved by any high-school student (or university professor)! No knowledge on Gröbner bases theory necessary!

A Suitable lc

lc[g1, g2] = lcm[lp[g1], lp[g2]]

is a suitable function that satisfies the above requirements.

Eureka! The crucial function lc (the "critical pair" function) in the critical pair / completion algorithm scheme has been synthesized automatically!

Case h1≠h2

In this case, df[h1,h2]∈G:

In this part of the proof (wich is much easier) we are basically stuck right at the beginning. By the requirement generation algorithm we obtain the following requirement for df:

({{(Underscript[∀ , h1, h2])(h1 (SuperStar[(Subscript[↓, {df[h1, h2]}])])h2), (df requirement).  }})

Looking to the Knowledge Base for a Suitable df

(Looking to the knowledge base of elementary properties of polynomial reduction, it is now easy to find a function df  that satifies (df requirement), namely

df[h1, h2] = h1 - h2,

because, in fact,

\(∀ \+\(f, g\)\(\((f\ \(\(↓\_{f - 
                        g}\)\^*\)g)\)\(.\)\)\)

Eureka! The function df (the "completion" function) in the critical pair / completion algorithm scheme has been "automatically" synthesized!)

An "Algorithm" for Algorithm Synthesis

Synthesis of a Gröbner Bases Algorithm

Conclusion

A way of looking at it ("what would have happened if ..."):

Pairs idea? (The CPC algorithm scheme did not really exist at that time.)

A[\(F, ⟨⟨g1, 
            g2⟩, p\&_⟩\)]=
where[f=lc[g1, g2],h1 = trd[rd[f, g1], F],h2 = trd[rd[f, g2], F],
{({{A[\(F, ⟨p\&_⟩\)], ⇐, h1 = h2}, {A[F⌢df[h1, h2],\(⟨p\&_⟩\)≍⟨⟨(Subscript[F, k]),df[h1, 
                                  h2]⟩ (Underscript[\[VerticalSeparator] , k = 
                                  1, …, \[LeftBracketingBar]F\[RightBracketingBar]])⟩], ⇐, otherwise}})} ]

Research Topics

Libraries of algorithm schemes.

More generally, libraries of formulae schemes for definitions, propositions, problems, and algorithms.

Case studies of problem (schemes), knowledge, algorithm schemes and how they produce algorithms.

How well are current reasoning systems suited for supporting this approach to algorithm (definition, theorem, problem, ...) synthesis?

Improved algorithms for generating problem specifications from failing proofs.

Automated synthesis of refinements of the S-polynomials-based Gröbner bases algorithm.

Automated synthesis of Gröbner bases algorithms not based on S-polynomials (do such algorithms exist?)

References

On Gröbner Bases

[Buchberger 1965]
B. Buchberger. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenrings nach einem nulldimensionalen Polynomideal. PhD Thesis, Mathematical Institute, University of Innsbruck, December 1965. (English Translation by Michael P. Abramson: "An Algorithm for Finding the Basis Element of the Residue Class Ring of a Zero Dimensional Polynomial Ideal",  Journal of Symbolic Computation,  Vol. 41 (Numbers 3-4), March / April 2006, pp. 475 - 511).

[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 2005]
B. Buchberger. 
Towards the Automated Synthesis of a Gröbner Bases Algorithm.
RACSAM (Review of the Royal Spanish Academy of Science), Vol. 98/1, pp. 65-75, 2005.

Appendix: The Proof Notebooks Automatically Generated by Theorema for the Synthesis of the Merge-Sort Algorithm

Notebook 1:

Pending proof of (13.4).

Pending proof of (8).

Notebook 2

Comment on Notebook 2: Note that in the knowledge base (i.e. the formulae listed under "assumptions"), the specification (Lemma (conjecture15): conjecture15)   is now contained, which describes the specification automatically generated (from the failing proof in Notebook 1) for the function 'special'. The proof then proceeds as in Notebook 1 but succeeds to get over the point at which the first proof was stuck.

Pending proof of (41.4).

Notebook 3

Comment on Notebook 3: Note that in the knowledge base (i.e. the formulae listed under "assumptions"), the additional specification (Lemma (conjecture44): conjecture44)   is now contained, which describes part of the specification automatically generated (from the failing proof in Notebook 2) for the functions 'left', 'right', and 'merge'. The proof then proceeds as in Notebook 2 but succeeds to get over the point at which the second proof was stuck.

Notebook 4

Comment on Notebook 4: Note that in the knowledge base (i.e. the formulae listed under "assumptions"), the additional specification (Lemma (conjecture46): conjecture46)   is now contained, which describes the second part of the specification automatically generated (from the failing proof in Notebook 3) for the functions 'left', 'right', and 'merge'. The proof then proceeds as in Notebook 3 but succeeds to get over the point at which the third proof was stuck and, actually, proceeds until the successful end.