Algorithmische Beweisverfahren
Das Ende der Mathematik?

Bruno Buchberger
RISC und RICAM
JK Symposium, 20. April 2005

Übersicht:

Algorithmische Beweisverfahren

Einige Beispiele (in Theorema)

Diskussion

Übersicht:

Algorithmische Beweisverfahren

Einige Beispiele (in Theorema)

Diskussion

Beweisen ist das, was Mathematik charakterisiert

Das Problem des Beweisens:

Gegeben: Eine Aussage A und Aussagen B.

Frage: Folgt A aus B ?  ("Wahrheits-Entscheider")

Gesucht: Eine korrekte Schlusskette, die A aus B herleitet.  ("Beweis-Finder")

Eine sehr viel schwächere Form des Beweisproblems:

Gegeben: Eine Aussage A,  Aussagen B und eine Schlusskette P.

Frage: Ist P eine korrekte Schlusskette, die A aus B herleitet.    ("Beweis-Prüfer")

Beispiel:

Aussage A:

(limit[f, a] ∧ 
          limit[g, b])      \[Implies]      limit[f + g, 
        a + b]

Aussagen B:

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

(f + g)[x] = f[x] + g[x]

etc.

Automatische Beweisprüfer: Z.B. Mizar

2000 Definitionen, 30.000 automatisch geprüfte Sätze.

Im Rahmen der Tarski-Grothendieck Mengenlehre (in Prädikatenlogik erster Stufe).

Von Mengenlehre bis Banach-Räume ...

Ca. 750 Artikel in Journal of Formal Mathematics.

A. Trybulec et al.,  University Bialystok, Polen, seit ca. 1976 (1989).

Automatische Wahrheitsentscheider, Beweisfinder:

Ist das möglich?

Bis zu welchem Grad?

Ist das wünschenswert?

Braucht es dann noch Mathematiker?

Braucht es dann noch Mathematik?

Wird sich die Art, Mathematik zu betreiben, ändern?

Übersicht:

Algorithmische Beweisverfahren

Einige Beispiele (in Theorema)

Diskussion

Das Theorema-Projekt

Ziel: Computer-Unterstützung des  Explorations-Prozesses mathematischer Theorien.

Die Theorema-Sprache ist eine Version der Prädikatenlogik.

Sie enthält eine Programmsprache.

Die Theorema-Gruppe: B. B., T. Jebelean, W. Windsteiger, T. Kutsia, M. Rosenkranz, F. Piroi, G. Regensburger, M. Giese  und  PhD- Studenten.

Viele andere Gruppen: ACL (Boyer, J.S. Moore et al.),  Coq , Elf (F. Pfenning), IMPS (W. Farmer et al.), Isabelle (L. Paulson), Nuprl (R. Constable et al.), Omega (J. Siekmann et al.), Otter (L. Wos) u.v.a.

Beispiel: Beweise in elementarer Analysis mit PCS-Beweiser

PCS-Methode: B.B. 2000,  D. Vasaru 2000;

Zu beweisen

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

Wissen

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

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

Wissen zusammenfassen

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

Aufruf des Beweisers

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

Beispiel: Beweise in Koordinaten-Geometrie mit Gröbner-Basen

Das Prinzip der Methode (B.B. 1965; B.B., S. Stifter, B. Kutzler 1986; D. Kapur 1986; F. Winkler 1990, J. Robu 2003):

Formula["Test",any[x, y],
	({{\(\((\ \ \((\(x\^2\) y - 3  x\ )\) ≠ 
                    0)\) ∨ \((\((x\ y + x + y)\) ≠ 
                    0)\) ∨ 
		\((\((\((\(x\^2\) y + 3  x = 
                            0)\) ∨ \((\((\(-2\)\ x\^2 + \(-7\)\ x\ y + 
                                x\^2\ y + 
                                x\^3\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2 + 
                                2\ x\^2\ y\^2)\) = 
                            0)\))\)
	 ∧ \((\((x\^2 + \(-x\)\ y + 
                            x\^2\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2)\) = 
                        0)\))\)\),           "B1"}})]

Prove[Formula["Test"], using -> {}, 
      by -> GroebnerBasesProver]

Beispiel einer Anwendung: Pappus Theorem

Graphisch

Seien A, B,  C und A1, B1,  C1 auf zwei Geraden und seien P = A B1 ⋂ A1 B, Q = A C1 ⋂ A1 C, S = B C1 ⋂ B1 C. Dann sind P, Q, und S kollinear.

In der Sprache der Geometrie  (Dissertation Dr. Judit Robu)

Proposition["Pappus",  any[A, B, A1, B1, C, C1, P, Q, S], 
      point[A, B, A1, B1] ∧ pon[C, line[A, B]] ∧ 
          pon[C1, line[A1, B1]] ∧ 
          inter[P, line[A, B1], line[A1, B]] ∧ 
          inter[Q, line[A, C1], line[A1, C]] ∧ 
          inter[S, line[B, C1], line[B1, C]] \[Implies] 
        collinear[P, Q, S]]

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> True}]

Der automatisch erzeugte Beweis

Beispiel einer Anwendung: Butterfly Theorem

Textbuch-Formulierung

A, B, C and D are four points on circle (O). E is the intersection of AC and BD. Through E draw a line perpendicular to OE, meeting AD at F and BC at G. Show that (OverBar[FE]) = (OverBar[GE]).

Sitzung mit dem Geo-Beweiser

Input to the system:

Proposition["Butterfly", any[O, A, B, C, D, EE, F, G], 
      point[O, A] ∧ 
pon[C, 
            circle[O, A]] ∧ 
pon[B, 
            circle[O, A]] ∧ 
pon[D, 
            circle[O, A]] ∧ 
inter[EE, line[A, C], 
            line[B, D]] ∧ inter[F, line[D, A], tline[EE, EE, O]] ∧ 
          inter[G, line[B, C], line[EE, F]]
 \[Implies] 
        distequal[EE, F, G, EE]]

Input to the system:

Simplify[Proposition["Butterfly"], 
      by -> GraphicSimplifier]

Output generated automatically by the system

End of output

Input to the system:

KnowledgeBase["Butterfly_g", 
      any[O, A, B, C, 
        D], {{ O, {100, 100}}, {A, {0, 100}}, {B, {55, 
            190}}, {C, {171, 170}}, {D, {60, 10}}}]

Input to the system:

Simplify[Proposition["Butterfly"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Butterfly_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Butterfly"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook

Übersicht:

Algorithmische Beweisverfahren

Einige Beispiele (in Theorema)

Diskussion

Einige Fragen:

Gibt es einen "universellen" Beweis-Finder für die gesamte Mathematik?

Was ist die praktische Alternative?

Kann man auch das Erfinden von Sätzen automatisieren?

Gibt es einen "universellen" Beweis-Finder?

Ja, z.B. A. Robinson's "Resolutionsverfahren", 1965.

War / ist (Haupt-) Forschungsgegenstand im Gebiet des automatischen Beweisens seit 1965.

Etliche Gruppen, Hunderte von Papers, z.B. Otter (L.Wos)

Kann man sich davon den Durchbruch für die Praxis des mathematischen Beweisens erwarten?

Warum nicht?

Alternative: Beweisen durch als korrekt bewiesene spezielle Beweis-Finder

Z.B.: Gröbner-Basen-Theorie (automatisch / computer-unterstützt) als korrekt bewiesen. (M. Bulo et al., in B.B., J. Campbell eds., Proc. of AISC 2004, RISC, Springer LNCS 3249, S. 171-184.)

Und dann Gröbner-Basen-Algorithmus als (wesentlichen Teil eines) speziellen Beweisers einsetzen.

Kann man auch das Erfinden von Sätzen automatisieren?

Ja, z.B. mit Methode des "Lazy Thinking" (Analyse von nicht erfolgreichen Beweisen), B.B. 1998.

Methode kann auch zum Erfinden von Algorithmen angewandt werden, B.B. 2003, A. Craciun 2003.

Automatische Generierung von Lemmata in Induktionsbeweisen:

Induktive Definition der Addition

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

Beweis, dass 0 auch Linksinverses ist

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

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

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

Beweisversuch für Kommutativität

Proposition["commutativity of addition",any[m, n],
	({{m + n = n + m, " + = "}})]

Prove[Proposition["commutativity of addition"],
	\(using -> ⟨Definition["addition"]⟩\),
	by -> NNEqIndProver,

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

Automatische Generierung von Lemmata aus dem erfolglosen Beweis

Theorema Algorithmus "Cascade" ("Lazy Thinking"): Automatische Analyse von Beweisobjekten und Erzeugen von Vermutungen.

\(\(Prove[Proposition["commutativity of addition"], 
	
        using -> Definition["addition"], 
        by -> Cascade[NNEqIndProver, ConjectureGenerator], 
        ProverOptions -> {TermOrder -> LeftToRight}];\)\)

Automatische "Erfindung" des Gröbner-Basenalgorithmus

Ein endliches multivariates Polynomsystem G ist eine Gröbner-Basis, wenn jedes Polynom bei allen möglichen "Divisionen" bzgl. G immer denselben "Rest" hat.  (Es gibt unendlich viele Polynome!)

Der wesentliche Satz: Um zu checken, dass ein Polynomsystem G die Gröbner-Basen-Eigenschaft hat, genügt es die Reste der endlich vielen "S-Polynome" aller Paare von G zu überprüfen.

S-Polynom[ g1, g2] :=  ein Polynom, das aus dem KGV  der "führenden Terme" in g1 und g2 gebildet wird.

Mit der obigen Methode der (automatischen) Analyse von (automatischen) erfolglosen Beweisen kann man Folgendes machen:

Man setzt einen Algorithmus an, der auf jedes Paar (g1, g2) von Polynomen aus G einen unbekannten Algorihtmus L anwendet und vom Ergebnis die Reste überprüft.

Der (automatische) Beweis der Korrektheit dieses "Algorithmus" schlägt natürlich fehl, weil L unbekannt ist.

Der automatische Beweisanalysator generiert eine Eigenschaft (Spezifikation) von L, der Erfülltsein den Korrektheitssatz zum Abschluss zu bringen gestattet.

Aus der automatisch erzeugten Spezifikation für L erkennt man "sofort", dass L[ g1, g2] im wesentlichen aus dem KGV der führenden Terme von g1 und g2 gebildet werden muss.

Damit ist der Gröbner-Basen-Algorithmus (plus Korrektheitsbeweis) im Wesentlichen automatisch "erfunden".

Automatisches Beweisen ist die natürliche Fortsetzung des Grundgedankens der Mathematik

Einmal nachdenken über das Allgemeine, erspart unendlich oft mal Nachdenken im konkreten Fall.

Mathematik führt zur Trivialisierung von Mathematik.

Glücklicherweise: Je mehr Mathematik durch mehr Mathematik trivialisiert wird, um so mehr nicht trivialisierte Mathematik tut sich auf.

Mögliche Konsequenzen für die Mathematik / Informatik Forschung, Ausbildung, Anwendung ?

Die Art, Mathematik zu erfinden, ihre Qualität zu kontrollieren, ihre Ergebnisse zu speichern und abzufragen, Mathematik zu unterrichten und anzuwenden wird sich (drastisch) ändern.

Der Computer ist für die Mathematik Forschungsgegenstand und Forschungswerkzeug (die "Kreativitätsspirale").

Die Ausbildung im formalem Denken ist ein Schlüssel zur Innovation.

Je mehr Arbeit von anderen gemacht werden kann, umso mehr müssen wir uns auf den jeweils höchsten Schichten der Arbeit profilieren.

Mathematical Knowledge Management: A Recent International Endeavor

The Theorema group is (an initiator and member) of the international MKM (Mathematical Knowledge Management) Network (NuPrl, Izabelle, MIZAR, ...)

Numerical Mathematics

Computer Algebra

Automated Theorem Proving

Mathematical Knowledge Management  
                                  ("Symbolic Computation" in its widest sense)

✓  The Theorema Project

An "Algorithm" for Algorithm Synthesis

Algorithmic Synthesis of a Gröbner Bases Algorithm

Conclusion

The Algorithm Invention ("Synthesis") Problem

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

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

Examples of specifications P:

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

A general algorithm S for "all" P cannot exist (cf. B. Caviness 1970, ...)   but ...

There is a rich literature on algorithm synthesis methods.

The "Lazy Thinking" Method (BB 2001): A Very Rough Sketch

Given: a problem specification P.

For finding an algorithm A that satisfies (Underscript[∀ , x]) P[x, A[x]],

- we generate (automatically) a couple of (hopefully) simpler problems Q, R, ...,

- we synthesize algorithms B, C, ...  for Q, R, ...

- from B, C, ... we compose (automatically) an algorithm A.

When can we terminate? 
When we arrive at problems, for which algorithms are already known.

The "Lazy Thinking" Method: More Details

Given a problem specification P

consider various "algorithm schemes" for A

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

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

From the temporary assumptions and goals in the failing proof situation (automatically) generate such specifications for the unspecified sub-algorithms that would make the proof possible.

Now, apply the method recursively to the auxiliary functions.

This is "lazy"

we use the condensed algorithmic experience of others (in the schemes)

we start (routine) proving before we have an algorithm

we just wait until we fail in order to get an idea from the failure.

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

(Underscript[∀ , x, y])(is–sorted⇔({{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

(Underscript[∀ , x])(sorted[x]={({{special[x], ⇐, is–trivial–tuple[x]}, {merge[sorted[left–split[x]],sorted[right–split[x]]], ⇐, otherwise}})})

("divide and conquer")

We Now Start Proving the Correctness Theorem and Analyze the Failing Proof

The Result of Applying Lazy Thinking

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]special[x]=x)

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

(Underscript[∀ , x])(left–split[x]≍right–split[x] ≈  x)

What Do We Have Now?

Case A: We find algorithms special, merged, left–split, right–split in our knowledge base for which the properties specified above are already contained in the knowledge base or can be derived from the knowledge base.
In this case, we are done, i.e. we have synthesized a sorting algorithm.

Case B: We do not find algorithms special, merged, left–split, right–split  in our knowledge base for which the properties specified can be proved.
In this case, we apply Lazy Thinking again in order to synthesize appropriate special, merged, left–split, right–split

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

How Can we Teach (= Automate) the Method

Compile a library of  "algorithm design experience" (= algorithm schemes).

Teach (automate) proving.

Teach (automate) generation of useful specifications of sub-algorithms from failing correctness proofs:

A simple (but amazingly powerful) rule:

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.

Research topic: other rules.

Parameters for Lazy Thinking

Lazy Thinking

Example: Synthesis of Insertion-Sort

Problem

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\&_⟩]\)])

Resulting Specification for Subalgorithms

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\&_⟩)\)}}) )

Details of an Automated Synthesis

See the notebooks automatically produced by Theorema for the insertion-sort example.

How far can we go with this method?

Can we automatically synthesize algorithms for non-trivial problems?

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

What is "non-trivial"?

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

Hence, question: Can Lazy Thinking automatically invent the notion of S-polynomial and automatically deliver the S-polynomial theorem.

✓  What we Have, What we Want

✓  An Algorithm for Algorithm Synthesis

Algorithmic Synthesis of a Gröbner Bases Algorithm

Conclusion

The Problem of Constructing Gröbner Bases

Find algorithm Gb such that

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

Definitions [BB 1965, 1970]:

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

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

(h1 (Subscript[-> , G])h2)⇔ (Underscript[∃ , g ∈ G])({({{lp[g] | lp[h1]}, {h2 = h1 - (lm[h1]/lm[g]) g}})} ),

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

Knowledge on the Concepts Involved

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

etc.

Algorithm Scheme "Critical Pair / Completion"

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

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

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

The Essential Problem

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

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

we can automatically produce the idea that

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

and

df[h1, h2]=h1-h2

and prove that the idea is correct.

Now Start the (Automated) Correctness Proof

With current theorem proving technology, in the Theorema system, the proof attempt could be done automatically. (Not yet fully implemented.)

Details

Upon Termination

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 Have to Prove

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

Assumption

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

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: In this case

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

Use Specification Generation Algorithm

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

Summarizing the Specifications of the Unknown Subalgorithm lc

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

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

and the requirements:

rd[lc[g1, g2], g1] ≺ 
      lc[g1, g2], 
rd[lc[g1, g2], g2] ≺ 
      lc[g1, g2],

which, in the case of the domain of polynomials, are equivalent to

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

A Suitable lc

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

is a suitable function that satisfies the above requirements.

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

Case h1≠h2 and, hence, 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 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)\)\(.\)\)\)

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

Namely,

Summary of the Synthesizing Proof Attempt

Failure Situation

The proof, of course, fails at the point where it would need knowledge about the unknown subalgorithms lc and df.

Beginning of the proof:

Let G be A[ F]. We have to prove that

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

Assumption

We only deal with the third, most important, property. For this, we assume

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

and have to find a polynomial g such that

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

Generation of the Specification of lc

In the failing proof situation, by the (automated) analysis algorithm sketched above, we detect that the proof could be completed if the unknown lc satisfied the following property:

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

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

Eureka! It is clear that this specification is (only) met by

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

Generation of the Specification of df

Similarly, it can be (automatically) detected that

df[h1, h2]=h1-h2.

✓  What we Have, What we Want

✓  An Algorithm for Algorithm Synthesis

✓  Algorithmic Synthesis of a Gröbner Bases Algorithm

Conclusion

Research Topics

Libraries of algorithm schemes.

More generally, libraries of definition, theorem, problem, and algorithm schemes.

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

Improved algorithms for generating problem specifications from failing proofs.

"Functor" knowledge: each algorithm is a "functor"

If s, m, l, r is a merge structure                                                then             A is a sort structure.
          and A results from s, m, l, r by divide and conquer

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 2004]
B. Buchberger. 
Towards the Automated Synthesis of a Gröbner Bases Algorithm.
RACSAM (Review of the Royal Spanish Academy of Science), Vol. 98/1, to appear, 10 pages.