Automated Mathematical Theory Exploration: How Far Can We Go?

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

Seminar "The Role of Computer Science in Science"
DERI, Innsbruck, December 14-15, 2006

The Scientific Approach

Mathematical Theory Exploration

A mathematical theory: axioms, definitions, theorems, problem specification, methods.

Mathematical theory exploration: the purest "intellectual" activity.

Automated Mathematical Theory Exploration

Automatic invention / proof of definitions, theorems, problems, methods.

We Need a (Universal) Language for Expressing Mathematical Theories

Predicate logic: Example of a formula

(Underscript[∀ , f,a ])limit[f, 
          a]⟺ (Underscript[((Underscript[∀ , ϵ])), ϵ > 0])(Underscript[∃ , N])(Underscript[((Underscript[∀ , n])), n ≥ N])\[LeftBracketingBar]f[n] - 
                    a\[RightBracketingBar] < ϵ

Language constructs:
    -  constants for objects, functions, predicates,
    -  variables,
    -  propositional connectives like '⟺',
    -  quantifiers like '∀', '∃'.

Higher order: variables for functions and predicates.

Examples are Taken from the Theorema Project

The Theorema project aims at prototyping features of a system for mathematical theory exploration.

The Theorema Group: B. B. (leader), T. Jebelean, W. Windsteiger, T. Kutsia, F. Piroi, M. Rosenkranz, M. Giese, and  PhD students.

The Theorema Language is a version of (higher order) predicate logic.

Some Automated Reasoners in Theorema:

- Predicate logic: natural deduction, S-decomposition
- Elementary analysis: PCS (alternating quantifiers)
- Set theory
- Induction on natural numbers, on tuples
- Equational logic with sequence variables
- Combinatorial identities
- Geometry (based on algebraic methods like Gröbner bases)
- Algorithms for symbolic functional analysis (boundary value problems)
- "Lazy Thinking" method for lemma and algorithm invention

Tools for structuring knowledge bases: functors, schemes, and others.
Computation within logic.
Two-dimensional user-definable syntax including "logicographic symbols".
Readable Proofs.

Meta-language: Mathematica.

Object language: higher-order predicate logic with sequence variables.

Example of Some Exploration Steps: The Notion of  Limit

Let's start from the situation:
-  we already have explored the theory of the reals with +, < ... "completely"
-  we already have explored the operations  ⊕, ... on sequences of reals

Introduction of the Notion of  Limit by a Definition

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

A Typical Theorem (How Do we Invent this Theorem?)

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

The PCS Method for Automated  Proving in Analysis (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.

Produces "natural" proofs that also contain algorithmic information.

Instead of a detailed explanation of the proof method, let's look to the proof generated for the above example of a proposition:

Initialize Theorema

(Automated) Proof of the Limit Theorema

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]\)]

Formulae from the knowledge base  generated in the previous exploration rounds:

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

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

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

Pack everything into one "theory":

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

Now call the prover:

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

The following proof is generated fully automatically by the PCS prover:

Problem: Computation of Limits

Find algorithm 'limit' such that

(Underscript[∀ , f])(is–convergent[f]⟹
          Limit[f, limit[f]])

This formula is the "specification" of the problem of limit computation.

Limit Algorithm: (How Do we Invent this Algorithm?)

We use the collection of knowledge which we proved for the notion Limit and use it as "rewrite rules".

The combination of these rewrite rule is a (first draft) of an algorithm meeting the above specification.

Now, Lifting Knowledge to Inferencing

After implementation of the proved knowledge on the predicate / function Limit on the meta-level as rules for the  quantifier lim, we can now compute (simplify) for example:

Compute[
      (lim_(n → ∞))[(5 + 
                1/n) (n/(2  n + 5))]]

Compute[
      (lim_(a → ∞))[(5 + 
                1/a) (a/(3  a + 5))]]

Compute[
      (lim_(n → ∞))[(((1 + 1/n))^n)]]

(The implementation is, however, not yet proved formally! An important goal for all theory exploration systems designed along these lines!)

What do we have to prove?  The application of the lim reasoning rules, without knowledge on Limit, have the same effect as using rewriting with the proved knowledge on Limit.

Two Ideas for Automating Mathematical Theory Exploration (BB 2002 ff.)

Formula Schemes: Condensed Experience for Inventing Axioms (Definitions), Theorems, Problems,  and Methods (Algorithms).

Conjectures from Failing Proofs: Failure has creative power!

Example: The Monotony Scheme and Limit Theorems

A typical scheme:

(Underscript[∀ , P, F, G])  (Monotony[P, F, G]⟺
(Underscript[∀ , a, b, f, g])(P[f, a]∧P[g, b])     \[Implies]     P[F[f, g],G[a, b]])

Given a knowledge base in which 'Limit', '+', and '+' occurs, we can apply the above scheme for "inventing" (proposing, conjecturing) a proposition:

Monotony[Limit, ⊕,+]

i.e.

(Underscript[∀ , a, b, f, g])(Limit[f, a] ∧ 
            Limit[g, b])      \[Implies]      Limit[
        f⊕g, a + b]

('Monotony' is a "relator" or (the description of) a "category". I cannot discuss  the important structuring power of  domains, categories, and functors in this talk.)

(I do not discuss the question here how the right substitutions for F and G can be automatically guessed. See, however, section 3 on algorithm synthesis: the creative power of analyzing failing proofs!)

The Role of Formula Schemes for Invention

By setting up a library of formula schemes, most formulae in the process of exploring a new notion can be generated automatically:

- propositions
- problems
- algorithms.

(Even, many interesting notions can be generated automatically by applying formulae schemes.)

Conjecture Generation from Failing Proofs

The idea:

- One tries to prove (automatically) a theorem.

- From a failing proof one (automatically) tries to extract an idea for lemmata whose truth may make the proof of the theorem possible.
- One then engages in the (automated) proof of the conjectured lemmata.
--- This process may be called recursively !  A "cascade" of conjectures (and, in the positive case, theorems) is automatically generated.

We show the power of this idea in a non-trivial example of automated algorithm invention!

What I want to illustrate with this example:

Algorithm synthesis: one of the aspects of mathematical theory exploration.

A combination of 
      -  (automated)  theorem proving
      -  (automated)  application of formula schemes for invention
      -  (automated) analysis of failing proofs

yields a powerful algorithm synthesis method ("lazy thinking method",  BB 2002).

Powerful: able to synthesize algorithms for non-trivial problems.

In particular, powerful enough to replace myself.

"Non-trivial"

Construction of Groebner bases:
               - at the time of invention (1965, BB) was conjectured to be 
                 algorithmically unsolvable
               - dozens of applications in algebraic geometry, invariant theory, optimization, 
                 coding theory, cryptography, symbolic summation, geo theorem proving,
                 graph theory,   ...,  origami proving,  sudoku solving,  ...
               - > 1000 papers, > 10 textbooks, > 3000 citations
               - not yet synthesized by other synthesis methods.

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

A general synthesis algorithm 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.

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

Algorithm Synthesis by "Lazy Thinking" (BB 2002)

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

We assume we have "complete" knowledge on the auxiliary notion appearing in P.

Consider known fundamental ideas ("algorithm schemes A") of how to structure algorithms A in terms of subalgorithms B, ... 
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.

Automated Invention of Sufficient Specifications for the Subalgorithms

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

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

and produce specification

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

Details: see papers [BB 2003] and example.

The method  works well on simple problems like sorting

See [Buchberger 2003].

For example, using the  divide-and-conquer scheme

(Underscript[∀ , N, S, M, L, R])Divide–and–Conquer[A,S,M,L,R]⇔
(Underscript[∀ , x])(A[x]={({{S[x], ⇐, is–trivial–tuple[
                        x]}, {M[sorted[L[x]],sorted[R[x]]], ⇐, otherwise}})})

the method finds (in approx. 2 minutes on a laptop) that all subalgorithms S, M, L, R satisfying the following specifications make A a correct sorting algorithm:

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

Now we can continue, recursively, with synthesizing - or retrieving - algorithms S, M, L, R satisfying the above specifications.

How Far Can We Go With Lazy Thinking

Successful synthesis of Groebner bases algorithm. See:

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.

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[->] :\(\(⇔\)\(∀ \+\(f1, f2\)\((f1\( ↔ \^*\)f2 \[Implies] 
              f1\(↓\^*\)f2)\)\)\)

The Essential Algorithmic Idea in Groebner Bases Theory (BB 1965)

It suffices to consider the reduction of

least–common–multiple[lp[g1], lp[g2]]

for all polynomials g1 and g2 in the basis F.

Hence, the Essential Methodologic Question for the Power of Algorithm Synthesis

Can we automatically produce the idea (and can we automatically prove the idea correct) that

least–common–multiple[lp[g1], lp[g2]]

are the essential objects we have to consider.

So let's start with the synthesis using the "lazy thinking" method.

We Assume that we Have "Complete" Knowledge on the Auxiliary Concepts Involved

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

etc.

Use Algorithm Schemes

For example: a scheme for any domain, in which we have a reduction operation 
           rd[ f, g]   (result of "reducing f by g")  satisfying  rd[f,g] ⪯ f 
           w.r.t. some Noetherian ordering ⪯.

(Underscript[∀ , A, lc, df])pair–completion[A,lc,df] ⟺

({{(Underscript[∀ , F])A[F] =A[F, pairs[F]]}, {(Underscript[∀ , F])A[F, ⟨⟩]=F
}, {\(∀ \+\(F, g1, g2, \(p\&-\)\)\)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}})} ]}})

(What would happen, if we started with another algorithm scheme, e.g. divide-and-conquer?)

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

First, it can be proved (independent of what lc and df are), 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 -> f1}, {p -> f2}})} )\[Implies]\(f1\(↓\^*\)f2\)).

Newman's lemma (1942):

is–Church–Rosser[ -> ]⇔ (Underscript[∀ , f, f1, f2])(({({{f -> f1}, {f -> f2}})} )\[Implies]\(f1\(↓\^*\)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 that lc[g1,g2] is reducible w.r.t. g1 and g2. The other cases are easy.)

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. In fact, it can be solved by high-school mathematics!

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

The automation of the mathematical invention and verification process
 is in the center of the 
 past, present, and future scientific / technologic spiral.

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.