Can Invention in Mathematics (Computer Science)
 be Automated ?

Bruno Buchberger
Research Institute for Symbolic Computation
Johannes Kepler Universität, Linz, Austria

Introduction and Summary

Algorithm Synthesis by "Lazy Thinking"

Synthesis of Gröbner-Bases Algorithm

Personal Remark

1965 - 1995:  Invention and Development of Groebner Bases Theory (Theorems, Algorithms, Applications)

1995 - 2010:  How to Automate Invention?

Today:  Invention of GB Theory can be Automated.

Can Invention in Mathematics (Computer Science) be Automated?

Yes and No !

Can Invention in Mathematics (Computer Science) be Automated?

Yes: By a theorem / algorithm (proved in finitely many steps) infinitely many inventions can be "automated".

Examples :

Theorem:  lim[f+g] = lim[f] + lim[g], ...
Theorem (Risch ~1970):  ∫f   =  a sum of exps and logs
Theorem:  A system (of non-linear multivariate polynomials) F has a common solution iff the Groebner basis of F is not {1}.
Theorem:  F is a Groebner basis iff  all S-polynomials of F reduce to zero.
Theorem: A geometrical statement S  is true iff  Poly(S) has no common solution.

Can Invention in Mathematics (Computer Science) be Automated?

Yes:

By non-trivial thinking, mathematics trivializes more and more non-trivial areas. ("It is the goal of mathematics to trivialize itself".)

Can Invention in Mathematics (Computer Science) be Automated?

No:

Never "all of mathematics" can be reached by one automated procedure. (Goedels Incompleteness Theorem.)

(Thus, mathematicians live in the best of all worlds!)

Can the Invention of Non-Trivial Algorithms (like the Groebner Bases Algorithm) be Automated?

This is the topic of today's lecture.

What Are Groebner Bases?

F = {(x^2)y - 2 x z + 5 y -3, 
       x (y^2) + (x^2) + z , 
       x z - (y^2) + 2 x -1}

GroebnerBasis[F]

{146302+448564 z+502763 (z^2)+242180 (z^3)+39771 (z^4)-6231 (z^5)-2448 (z^6)+168 (z^7)+144 (z^8)+16 (z^9),104376175362406+1599126115499 x+285345650746687 z+259094430962640 (z^2)+81019429651948 (z^3)-562741124769 (z^4)-4290216888948 (z^5)-216539112184 (z^6)+199291173968 (z^7)+31903397104 (z^8),-29252096339198961+996255569955877 y-79297437999899296 z-73993371970407310 (z^2)-24666034475337294 (z^3)-250747610968661 (z^4)+1288154187383705 (z^5)+85610415996090 (z^6)-58609022325772 (z^7)-10267480080072 (z^8)}

Anwendungsbeispiel:  "Algebraic Biology" 2007, RISC, S. Petrovic et al.

Gegeben:

Gesucht:

x, y, z, ...:  Wahrscheinlichkeiten an den Knoten des Ähnlichkeits-Baums.

Anwendungsbeispiel:  Software Reverse Engineering,  2007, RISC, T. Jebelean, D. Kapur, ...

Gegeben:  Programm.

Gesucht:   Spezifikation.

Bzw.

Gegeben:  Programm, Spezifikation.

Gesucht:   Schleifeninvarianten für die formale Verifikation.

x, y, z, ...:  die Werte der Programmvariablen.

Anwendungsbeispiel: 
Brechen eines kryptographischen Codes, 
2003, Paris VI, J.C. Faugere et al.

Gegeben:  Input - Output Textbeispiel

Gesucht:   Der Schlüssel,  z.B.    011000101011011....11011101.

x, y, z, ...:  die Bits im Schlüssel.

Example of Application: "Algebraic Oil", 
Shell 2005,  RISC 2009

Given:  Observation of the yield in dependence on the position of the valves.

Find:   The coefficients of a polynomial system that describes this dependence.

x, y, z, ...:  the positions of the valves.
Solved by Groebner bases 2005.

Relevance of Groebner Bases

Dozens of (difficult) problems on non-linear systems can be reduced to the construction of Groebner bases 
 (~ 1000 papers, ~ 30 books,  own AMS Classification number: 13P10).

Some of these problems were open for many decades.

Solution of these problems is possible for Groebner bases, because Groebner bases have some nice properties  (canonicality, elimination, syzygy property).

Therefore the construction of Groebner bases is an important problem.

Definition of Gröbner Bases  (BB 1965)

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

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

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

is–confluent[->] :⇔(Underscript[∀, f1,f2])(f1(SuperStar[↔])f2\[Implies]f1(SuperStar[↓])f2)

Example of a Property of Gröbner Bases: Elimination Property

A Gröbner bases G (w.r.t. a lexicographic ordering) is "triangularized" (see the example at the beginning)!

This allows to obtain all the solutions of G by successive elimination.

F = {(x^2)y - 2 x z + 5 y -3, 
       x (y^2) + (x^2) + z , 
       x z - (y^2) + 2 x -1}

GroebnerBasis[F]

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

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.

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

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

The power of the Gröbner bases method is contained in the invention of the notion of S-polynomial and the proof of the above theorem.

S-Polynomials

(Subscript[f, 1])=-2y+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

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 main theorem is available.

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.

Example

F = {(x^2)y - 2 x z + 5 y -3, 
       x (y^2) + (x^2) + z , 
       x z - (y^2) + 2 x -1}

GroebnerBasis[F]

Introduction and Summary

"Lazy Thinking"

Synthesis of Gröbner-Bases Algorithm

The "Lazy Thinking" Method

Is a method for the systematic invention of algorithms.

The method can be automated if suitable automated reasoners are available.

The Theorema system (BB et al. 1996 -  ) is a possible frame for the automation of the method.

Defining, Conjecturing, Proving, Programming, Computing  in Theorema

Load Theorema

Needs["Theorema`"];

Define and Conjecture

Definition["addition",any[m,n],
	({{m+0=m, " +0:"}, {m+(SuperPlus[n])=(SuperPlus[(m+n)]), " + .:"}})]

Proposition["left zero",any[m,n],
	({{0+n=n, "0+"}})]

Prove

Prove[Proposition["left zero"],
	using->⟨Definition["addition"]⟩,
	by->NNEqIndProver,

	ProverOptions->{TermOrder->LeftToRight},transformBy->ProofSimplifier,TransformerOptions->{branches->{Proved}}];

Automatically Generated Proof

Compute

Compute[(SuperPlus[(SuperPlus[0])])+(SuperPlus[(SuperPlus[(SuperPlus[0])])]),using->⟨Definition["addition"]⟩]

Another Example of Defining, Conjecturing, Proving, ...

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

Definition["limit:",any[f,a],
	limit[f,a]⟺ (Underscript[(Underscript[∀, ϵ]), ϵ>0])(Underscript[∃, N])(Underscript[(Underscript[∀, 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!

Automatically Generated Proof

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–sorted–version[x,y]

P[x,y] ⇔ is–integral–of[x,y]

P[x,y] ⇔ is–Gröbner–basis[x,y]
....

Algorithm Synthesis by "Lazy Thinking" (BB 2002)

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

Given: A problem (specification) P.           Find: An algorithm A for P.

Overall Strategy of Lazy Thinking:  (Automatically) reduce problem P to a couple of (hopefully simpler) problems  Q, R, ...

until ...

Two Key Ideas of Lazy Thinking

Given: A problem (specification) P.           Find: An algorithm A for P.

(Understand the problem "completely": Specification P must be spelled out and  "complete" knowledge must be available on the notions that occur in the specification P.)

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

For the chosen scheme A, try to prove   (Underscript[∀, x]) P[ x, A[x]]: From the failing proof construct specifications for the subalgorithms B occurring in A.

Example of an Algorithm Scheme ("Divide and Conquer"):

(Underscript[∀, x])(A[x]={({{S[x], ⇐, is–trivial–tuple[x]}, {M[A[L[x]],A[R[x]]], ⇐, otherwise}})})

A  is unknown algorithm.

S, M, L, R  are unknown subalgorithms.

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.

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

And the work of A. Bundy and his group (U of Edinburgh) on the automated invention of induction schemes.

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

Problem: Synthesize algorithm "sorted" such that

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

("Correctness Theorem")

Knowledge on the Problem:

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

is–sorted[⟨⟩]

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

(Underscript[∀, x,y,(OverBar[z])])(is–sorted[⟨x,y,(OverBar[z])⟩]⇔({{x≥y}, {is–sorted[⟨y,(OverBar[z])⟩]}}))

etc. (approx. 20 formulae, see notebook of proofs in the Appendix.)

An Algorithm Scheme: Divide and Conquer

(Underscript[∀, x])(A[x]={({{S[x], ⇐, is–trivial–tuple[x]}, {M[A[L[x]],A[R[x]]], ⇐, otherwise}})})

sorted  is unknown algorithm.

S, M, L, R  are unknown subalgorithms.

The only thing known is how the unknown algorithm sorted is composed from the unknown algorithms  S, M, L, R.

We now start an (automated) induction prover for 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[X,...m  [Y] ] ).

Details: see papers [Buchberger 2003] and example (in appendix).

The Result of Applying Lazy Thinking in the Sorting Example

Lazy Thinking, automatically (in approx. 1 minute 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 !

What do we have now: A problem reduction !

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⟩]
(Underscript[∀, x,(OverBar[y])])(A[⟨x,(OverBar[y])⟩]=i[x,A[⟨(OverBar[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⟩)
(Underscript[∀, x,(OverBar[y])])(is–sorted[⟨(OverBar[y])⟩] \[Implies]({{is–sorted[i[x,⟨(OverBar[y])⟩]]}, {i[⟨x,(OverBar[y])⟩] ≈ (x⌣⟨(OverBar[y])⟩)}}) )

Introduction and Summary

"Lazy Thinking"

Synthesis of Gröbner-Bases Algorithm

How Far Can We Go With the "Lazy Thinking" 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.

"Non-trivial" part of the invention: The invention of the notion of S-polynomial and the characterization of Gröbner-bases by finitely many S-polynomial checks.

With the "Lazy Thinking" method, it is possible to invent the essential idea of Buchberger's Gröbner bases algorithm (1965) fully automatically: See [Buchberger 2005, Craciun 2008].

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

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

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

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

is–confluent[->] :⇔(Underscript[∀, f1,f2])(f1(SuperStar[↔])f2\[Implies]f1(SuperStar[↓])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⟩,(OverBar[p])⟩]=
where[f=lc[g1,g2],h1=trd[rd[f,g1],F],h2=trd[rd[f,g2],F],
{({{A[F,⟨(OverBar[p])⟩], ⇐, h1=h2}, {A[F⌢df[h1,h2],⟨(OverBar[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]].}}))

using the above scheme for A  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 can be done automatically. 
( PhD thesis 2008 by my  student 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],F],h2=trd[rd[f,g2],F],∨{({{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->f1}, {p->f2}})} )\[Implies]f1(SuperStar[↓])f2).

Newman's lemma (1942):

is–Church–Rosser[->]⇔ (Underscript[∀, f,f1,f2])(({({{f->f1}, {f->f2}})} )\[Implies]f1(SuperStar[↓])f2).

Definition of "f1 and f2 have a common successor":

f1(SuperStar[↓])f2 ⇔ (Underscript[∃, g])({({{f1(SuperStar[->])g}, {f2(SuperStar[->])g}})} )}

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(SuperStar[(Subscript[->, G])])g,}, {f2(SuperStar[(Subscript[->, 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](Subscript[->, g1])rd[lc[g1,g2],g1](SuperStar[(Subscript[->, G])])trd[rd[lc[g1,g2],g1],G]=
trd[rd[lc[g1,g2],g2],G](SuperStar[(Subscript[←, G])])rd[lc[g1,g2],g2](Subscript[←, 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,

(Underscript[∀, a,q])( a q lc[g1,g2](Subscript[->, g1])a q rd[lc[g1,g2],g1](SuperStar[(Subscript[->, G])])a q trd[rd[lc[g1,g2],g1],G]=
a q trd[rd[lc[g1,g2],g2],G](SuperStar[(Subscript[←, G])])a q rd[lc[g1,g2],g2](Subscript[←, 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(Subscript[->, g1])rd[p,g1]=a q rd[lc[g1,g2],g1](SuperStar[(Subscript[->, G])])a q trd[rd[lc[g1,g2],g1],G]=a q trd[rd[lc[g1,g2],g2],G](SuperStar[(Subscript[←, G])])a q rd[lc[g1,g2],g2]=rd[p,g2](Subscript[←, g2])p}

and, hence,

f1(SuperStar[(Subscript[->, G])])a q trd[rd[lc[g1,g2],g1],G],

f2(SuperStar[(Subscript[->, 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

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](lc[g1,g2]|p)) ,

and the requirements:

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

Now this problem can be attacked independently of any Gröbner bases theory, ideal theory etc.

A Suitable lc

lcp[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 we are basically stuck right at the beginning.

We can try to reduce this case to the first case, which would generate the following requirement

({{(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,

(Underscript[∀, f,g])(f (SuperStar[(Subscript[↓, {f-g}])])g).

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

Automation of mathematical reasoning ("formal methods") is in the center of the technology spiral:

Mathematics / Computer Science is the most exciting study and research field of our times.

On my "Thinking, Speaking, Writing" Course

B. Buchberger.
Thinking, Speaking, Writing: A Course on Using Predicate Logic as a Working Language.
Lecture Notes, RISC (Research Institute for Symbolic Computation), Johannes Kepler University,  Linz, Austria, 1982 - 2007.

On my "White Box / Black Box Principle" for the Didactics of Using Math Software Systems for Math Teaching

B. Buchberger
Should Students Learn Integration Rules?
ACM SIGSAM Bulletin Vol.24/1, January 1990, pp. 10-17.

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 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, 2005, pp.  65-75.

[Craciun 2008]
A. Craciun. 
The Implementation of Buchberger's Lazy Thinking Method for Automated Algorithm Synthesis in Theorema.
PhD Thesis, Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria, April 2008.

First Proof Attempt

Pending proof of (13.4).

Pending proof of (8).

Second Proof Attempt (with Specifications of Subalgorithms Extractd from First Proof Attempt)

Pending proof of (41.4).

Third Proof Attempt (with Specifications of Subalgorithms Extractd from Second Proof Attempt)

Successful Proof (with Specifications of Subalgorithms Extractd from Third Proof Attempt)