Mathematical 
Theory Exploration

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

Invited Talk at IJCAR 2006 
Seattle, USA, August 17 - 20, 2006

Copyright Bruno Buchberger 2006
Copyright Note: This file may be copied, distributed, and stored under the following conditions:
- The file is kept unchanged including this copyright note.
- A message is sent to bruno.buchberger@jku.at.
- If material from this talk is used, this talk should be cited appropriately.

The Simple Message

-  To the automated reasoning community:
    Mathematics is the main target! ...
    
-  To my fellow mathematicians:  
    Mathematics is  (automated) reasoning. ...

Automated Reasoning: Little Impact on Mathematics.

"Mathematics": mathematical theory exploration

for example, writing lecture notes on analysis,

for example, writing a research monograph on Groebner bases theory,

for example, doing research on the Poincare conjecture,

for example, writing a paper for a journal,

for example, re-organizing the knowledge in a journal for checking the originality of results,

...

I do not mean: automation of mathematical "intuition"

Mathematical exploration is an alternation between "hot" (intuitive) and "cool" (formal) phase.

It is good enough if we can give significant algorithm-support to the cool phases.

However:

-  formal theory exploration is one source of intuition,
      -  intuition often comes from consideration of examples;  formal reasoning (computation) supports this.
      -  intuition often comes from failing proof (algorithm ...) attempts;  formal reasoning can support this.

Automated Reasoning: Little Impact on Mathematics.    Why?

no algorithm libraries in automated reasoning systems (exceptions: ...)

no mathematical knowledge bases (exceptions: ...)

syntax, proof presentation, ... not attractive

little attention to special theorem proving (vs. general theorem proving)

little attention to "mathematical theory exploration" (vs. isolated theorem proving)

little attention to "proof generation" (vs. "proof checking")

little attention to "migration through reasoning levels" (vs. one-level reasoning)

a social reasons: "the mathematicians"

Automated Mathematical Theory Exploration: Time is Ripe

software technology

front-ends: ..., 2-dimensional syntax, "screen and keyboard" instead of "paper and pencil", ...

hardware

mathematical logic and automated reasoning

structural build-up of "all of mathematics"  (Bourbakism)

tremendous advances in algorithmic mathematics (discrete, algebraic, symbolic, ...)

an international community on "automated mathematical theory exploration": QED, Calculemus, MKM, ...

The Way to Go: Systems for Mathematical Theory Exploration

predicate logic as the working language

-  predicate logic is "practical"
          -  writing in logical syntax (as opposed to "pretty printing")
          -  algorithms and theorems expressed in one language 
          -  reasoners:  provers, solvers, simplifiers
          -  object level and meta-level expressed in one language: prove (special) reasoners correct

The Way to Go: Systems for Mathematical Theory Exploration

put effort also into special reasoners (as opposed to general reasoners)

"computer algebra and automated theorem proving": 
        - RISC PhD Curriculum 1982
        - JSC editorial 1985
        - Calculemus Group 1995
        - forthcoming book by J. Harrison.

The Way to Go: Systems for Mathematical Theory Exploration

put effort also into automated proof generation (as opposed to automated proof checking)

do not (always) look at "first principles": there are four possibilities:

build-up    - from "first principles"                      -  by "first principles"
                 - from "intermediate principles"         - by "intermediate principles"

create the logic frame for "proving reasoners correct":

build-up    - from "first principles"                      -  by "first principles"
                 - from "intermediate principles"         - by "intermediate principles"

focus on the 99 % of "easy" reasoning in theory exploration

("easy" is a relative concept anway!)

The Way to Go: Systems for Mathematical Theory Exploration

support also invention of mathematical knowledge: e.g. by schemes and learning form failure

support structured build-up of mathematical knowledge:

- categories / functors 
               - "completion of knowledge"
               - "mathematical personalities"
               - algorithmic knowledge
               - "(anti)-Bourbakism of the 21st century"

The Way to Go: Systems for Mathematical Theory Exploration

the next generation of mathematicians: formally and algorithmically trained

The Way to Go: Systems for Mathematical Theory Exploration

the future of the organization of mathematics: formal-reasoning based

- build-up of globally accessible mathematical 
                 (non-algorithmic and algorithmic) knowledge bases
               - refereeing
               - knowledge retrieval
               - knowledge self-expansion
               - re-structuring (expression of "mathematical personalities")

An indicator: the NIST project on "Handbook of Special Functions" (Abramovitz, Stegun; chapter on "computer algebra" by F. Chizak and P. Paule).

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.

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.

The Exploration Process:  A Spiral

Examples of Rounds through the Spiral

Difficult       Introduction      Properties    Easy        Lifted
 Proving                               up to           Proving    Proving
                                            saturation
 --------------------------------------------------------------------------------------

induction     x+0=x              arithm.laws   rewriting   count '   
                    x+y'=(x+y)'                                           sort vars

Examples of Rounds through the Spiral

Difficult         Introduction      Properties    Easy        Lifted
 Proving                                 up to            Proving    Proving
                                              saturation
 --------------------------------------------------------------------------------------

Equational     group              7 more         normal f.  simplification      
 logic              axioms             equalities     rewriting  to group nf.
                                              by mgu
                                              interaction

Examples of Rounds through the Spiral

Difficult         Introduction      Properties    Easy           Lifted
 Proving                                 up to            Proving       Proving
                                              saturation
 --------------------------------------------------------------------------------------

pred. log.     def. of              S-poly          rewriting       ideal       
 set th.          Groebner          theorem       w.r.t.            membersh.
                     bases               ...                ideal props.  by Groebner
                                                                                    bases

Examples of Rounds through the Spiral

Difficult         Introduction      Properties    Easy           Lifted
 Proving                                 up to            Proving       Proving
                                              saturation
 --------------------------------------------------------------------------------------

simple          geo notions       propos.           ???          ???
 pred. log.     after                  about 
 plus             coordinat.          configurations
 Groebner b.                    
 algorithm

Examples of Rounds through the Spiral

Difficult         Introduction      Properties    Easy           Lifted
 Proving                                 up to            Proving       Proving
                                              saturation
 --------------------------------------------------------------------------------------

pred. logic    definitions        boolean        rewriting      boolean
                     of ⋃, ⋂, ...       algebra                            algebra
                                             propert.                           simplifier

Examples of Rounds through the Spiral

Difficult         Introduction      Properties    Easy           Lifted
 Proving                                 up to            Proving       Proving
                                              saturation
 --------------------------------------------------------------------------------------

pred. logic    axioms of         delineability  reduce         Collins'
                     real closed       theorem       quants.        cylindrical
                     fields                                    to                 alg. decomp. 
                                                                 finite 
                                                                 connectives

Examples of Rounds through the Spiral

Difficult         Introduction      Properties    Easy           Lifted
 Proving                                 up to           Proving       Proving
 --------------------------------------------------------------------------------------

PCS              def. of             rewrite laws  rewriting      inference
 (pred. log.     limit                 for limit                            rules
 plus                                                                             for limit
 Collins'                                                                        quantifier
 algor.  )

More Details about Limit Exploration

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 Limit

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

(Please, don't torture me with questions on types!)

A Typical Interaction of New Notion with Previous Notions

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

Such Properties can be Invented Automatically by Schemes

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

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.

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

The Corresponding Part of the Theorema Session

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:

At Saturation Point

We have a situation where inventing more propositions is uninteresting because more complicated propositions can be reduced to the already proved ones by "easy" proving, namely rewriting ("symbolic computation", "high school proving", "physicists proving", ...).

I.e. no point in proving:

limit[f + g + h]  =  limit[f] + limit[g] + limit[h]

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.

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

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.