Lazy Thinking:
A New Method 
for Algorithm Synthesis

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

Computer Mathematics

Numerics

Computer Algebra

Computational Logic

...

Unification, Interaction

Computational Algebra and Logic: BB.,  Editorial of J of Symbolic Computation 1985; Theorema 1995; ... "Calculemus":

Apply algebra to logic (e.g. Gröbner bases for geo theorem proving, ...)

Apply logic to algebra (e.g. automated verification and synthesis of algebraic algorithms, ...)

Computational Algebra and Numerics / Functional Analysis: SFB "Scientific Computing", Radon Institute RICAM, ...

E.g. numerical Gröbner bases (H. Stetter's book), ...

E.g. SFB 1322, Gröbner bases for operator theory, see talk by M. Rosenkranz

E.g. Special Semester on Gröbner bases at RICAM and RISC (Feb - July 2006): 
                              Workshop "Approximate Commutative Algebra"  (Feb 20-26, 2006)

The Theorema Project

The Theorema project at RISC aims at prototyping a system in wich the entire process of inventing and verifying mathematics ("mathematical theory exploration") should be supported:

- "automated proof generating" paradigm

- not "automated proof checking" paradigm.

A uniform logic and software frame: higher order predicate logic for both reasoning and computing.

Implementation language: Theorema.

Acknowledgement: T. Jebelean, W. Windsteiger, T. Kutsia, F. Piroi, M. Rosenkranz, and PhD students.

Some Reasoners in Theorema

- Predicate logic: natural deduction, S-decomposition
- Elementary analysis: PCS (alternating quantifiers)
- Set theory
- Induction on natural numbers, on tuples, ...
- Functors
- Equality, sequence variables
- Combinatorial identities
- Geometry (based on algebraic methods like Gröbner bases)
- "Lazy Thinking" method for algorithm synthesis 
- ...

The PCS Method for Analysis Proving (BB 2001)

This method reduces proving in elementary analysis (formulae with "alternating quantifiers" on functions) systematically to the solution of inequalities over the real numbers.

A Proof Generated by PCS

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]

The following proof is generated completely automatically by this call to the PCS prover:

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

Algorithm Synthesis by "Lazy Thinking" (BB 2002)

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

Given: A problem P.           Find: An algorithm A for P.

Learn how to prove.

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

Collect (discover, prove) "complete" knowledge on the auxiliary notion appearing in the problem 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.

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 "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])(sorted[x]={({{S[x], ⇐, is–trivial–tuple[x]}, {M[sorted[L[x]],sorted[R[x]]], ⇐, otherwise}})})

S, M, L, R  are unknowns.

We now start an (automated) induction prover for proving the correctness theorem and analyze the failing proof: see notebooks in the appendix 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 !

What Do We Have Now?

Case A: We find algorithms S0, M0, L0, R0 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 S0, M0, L0, R0   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 was open for about 60 years.

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

What are Gröbner Bases?

(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]]

Definition of Groebner Bases

A set F of polynomials is called a Groebner basis (w.r.t. a chosen ordering of power products) iff

(Subscript[-> , F]) is confluent.

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

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

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

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.

Proof: Nontrivial. Combinatorial. Some details see below.

The theorem reduces an infinite check to a finite check:  Recall definition of "F is a Gröbner basis":
          for infinitely many (Subscript[f, 1]), (Subscript[f, 2]) one has to ...
          
 Remark: If F is a Gröbner basis then it has many other other useful properties (e.g. "elimination property").

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

S-Polynomials: The Main Notion of Algorithmic GB Theory

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

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

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

The Meta-Problem of Automatically Finding an Algorithm for Constructing Gröbner Bases: Apply "Lazy Thinking"

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.

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

using the above scheme for A  we can automatically produce the idea of S-polynomial,  i.e. the idea that

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

and

df[h1, h2]=h1-h2

are suitable choices in the algorithm scheme.

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.

Ongoing PhD thesis by 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\(↓\^*\)f2\)).

Newman's lemma (1942):

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

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

\(f1\(↓\^*\)f2\) ⇔ (Underscript[∃ , g])({({{\(f1\( -> \^*\)g\)}, {\(f2\( -> \^*\)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\(\( -> \_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

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

({{\(∀ \+\(h1, h2\)\((h1\ \(\(↓\_{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!)

Theorem proving methods, together with suitable strategies for systematic mathematical theory exploration, are reaching a level of sophistication where the automated invention of correct non-trivial algorithms seems to be possible.

This is just one aspect of the overall goal of formal mathematics: Create an environment of reasoning tools for building up large, provenly correct, well structured, formal mathematical knowledge bases (concepts, propositions, problems, algorithms).

"(Anti-) Bourbakism of the 21st Century".

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