A Formal Knowledge Base 
for Groebner Bases Theory

Bruno Buchberger

RISC and RICAM
Linz, Austria
Bruno.Buchberger@RISC.Uni-Linz.ac.at

Talk at the Annual Meeting 
of the Japanese Society for Symbolic and Algebraic Computation (JSSAC) 
Atsugi, Japan, September 1-4, 2004

Copyright Bruno Buchberger 2004

Copyright Note: Copying and storing is granted under the following conditions:

-  The file is kept unchanged (including the copyright note)
-  A message is sent to Bruno.Buchberger@RISC.Uni-Linz.ac.at
-  If the material in this talk is used in publications or talks, please, cite the talk appropriately.

Motivation

Summary of Motivation

This is a research plan not a report on research already done.

1st motivation: special semester on Groebner bases at RICAM / RISC, Feb - July 2006.

2nd motivation: a benchmark for Mathematical Knowledge Management (MKM) tools.

3rd motivation: preparation for an interactive book on Groebner bases.

Special Semester at RICAM / RISC

The RICAM / RISC  special semester on Groebner bases will have the following structure:

The build-up, expansion, and maintenance of a formal knowledge base on Groebner bases theory will be one of the key activities of all phases of the special semester.

A Benchmark for MKM Tools

The various MKM tools (algorithmic reasoners and organizational tools), e.g. the Theorema systems, can only be assessed and improved if we work with mathematical knowledge bases of realistic size.

In toy examples, the real problems of MKM do not become manifest.

Interactive Book on Groebner Bases

The kernel of the book should be written completely in predicate logic so that algorithmic processing of all the formulae in the book will be possible.

What is a formal knowledge base? What does it mean to "process" formulae? Are LaTeX formulae formal?

What Can We Do with Current Mathematical Papers?

A Sample Paper

Title

Abstract

Body of the Paper

See other window.

Possible Actions

( If it is real paper, one can do origami. )

Read and "understand"

Summarize the essence

Compare it with what is known

Knowledge base:

in one's head

other papers

implemented algorithms in math software systems

Implement an algorithm

Program the algorithm in an existing programming language.

Apply an algorithm to examples

Compare a definition or proposition

Is this definition known? 
Is it equivalent to an existing one? 
Is it "correct"? 
In which context is it meaningful?

(Note: all this is relative to a "knowedge base" K.)

Similarly for a proposition:

Similarly for mixed text.

Check a proof

Is the proof correct? Implicit assumptions? Most general form? New?  (What is the knowledge base behind it?)

Apply definitions to examples, counter-examples

Check (compute, prove) whether the properties asserted hold?

(What is the knowledge base now?)

Include references

What do we have to do for checking the example? Where is the knowledge base?

Assess the complexity of an algorithm

Invent

Based on the inspiration obtained from the paper, invent (variants of the)

definitions, 
theorems, 
problems,
algorithms,
examples,
etc.

...

What We Cannot Do with Current Mathematical Paper

Algorithmic Reasoners

For some of the above actions, we have "meta"-algorithms that support these actions

programming language (interpreters and compilers) that apply programs to input

proof-checkers that check whether a given proof is correct

decision methods for special theories (that check whether or not a given proposition in the theory is correct)

proof generators that generate proofs for correct propositions

special checkers that check whether a given formula occurs or is equivalent to a known formula

algorithm synthesizers that generate algorithms from specifications

algorithm verifiers that prove the correctness of algorithms w.r.t. specifications

invention algorithms for definitions and problems (based on "schemes")

invention propositions (based on "schemes" and algebra)

model checkers that generate examples and counter examples

....

The collection of these tools is called "mathematical theory exploration tools" or "mathematical knowledge management (MKM) tools".

(Note: The scope of MKM tools is wider. It includes also "organizational" tools.)

More and better reasoning tools: a hot research topic.

Not Applicable to Current Papers

However, all these tools only work for "formal" knowledge (goals and assumptions)

"Formal" knowledge: Expressed in a language whose syntax, semantics and/or pragmatics is defined in a meta-language.

Pragmatics: Inference mechanism (logic languages) or computational mechanism (programming languages).

These tools are, therefore, not applicable to the majority of the current papers.  (Note that this is also true for papers coded in LaTeX, MathML etc.! Why not?)

Hence, formal knowledge bases are a necessity for future MKM

The currently biggest formal mathematical knowledge base is the MIZAR library.

However, the proof paradigm of MIZAR is confined to proof checking.

I think that this paradigm is not sufficient for realistic computer-supported mathematical theory exploration.

The Theorema project is one of the alternative projects  that emphasize computer-supported proof generation.

In the long run (hopefully, in the near future) all relevant mathematical papers should be "formal"

I advocate that (the essential kernel of) future math papers should be written in a completely formal way so that they can be processed by the available reasoners (MKM tools).

Along with this, completely formal knowledge bases of the essential results in the existing literature should be build-up.

Formalization is a Nontrivial Process

Examples

Example

A formalization in Theorema (predicate logic):

(Underscript[∀ , X,  < ])(is–admissable–order[X,  < ]⇔
({{is–total–order[<,T[X]]}, {\(∀ \+\(t ∈ T[X]\{1}\)1 < t\)}, {(Underscript[∀ , s, t, u ∈ T[X]])(s < t \[Implies] 
                      s . u < t . u)}}))

Note various subtleties:

< is an essential parameter!

the scope of the quantifiers is not completely clear in the original text

in the original text, T[X] is OK (necessary) on the right-hand side, whereas it is disastrous on the left-hand side.

1 and . are hidden parameters. Where do they come from?

1 = ((Subscript[x, 1])^0) .  ((Subscript[x, 2])^0)  ...  ((Subscript[x, n])^0)is a hidden definition within a definition. What should we do with this? Where does the n come from?

The use of "functors" and "categories":

Definition of a "category" (in a nutshell):

(Underscript[∀ , X,  < ])(is–admissably–ordered[
            D, <,1,.]⇔
({{is–totally–ordered[D,  < ]}, {is–constant[D, 1]}, {is–binary–function[
                  D,  . ]

                }, {\(∀ \+\(t ∈ D\{1}\)1 < t\)}, {(Underscript[∀ , s, t, u ∈ D])(s < t \[Implies] 
                      s . u < t . u)}}))

Definition of a "functor" (in a nutshell) that produces the domain of power products T with operations 1 and .  from a set of indeterminates X:

is–power–product–domain–over[T, 
          1, .,X]⇔ ...

Now:

(Underscript[∀ , X,  < ])(is–admissable–order[X,  < ]⇔  (Underscript[∃ , T, 1,  . ])(({{is–power–product–domain–over[T, 
                      1, .,X]}, {is–admissably–ordered[
                      T, <,1,.]}})))

A Functor

Functors (and categories) allow concise presentation of big portions of mathematical knowledge:

Definition["Groebner extension" ,any[R],
Groebner–extension[R]   =Functor[N,\(any[C, k, p, p\&_, q, q\&_, x, X, y, y\&_, Y]\),
	({{𝕤 = ⟨⟩}, {({{
(Underscript[ϵ, N])[
                              x] ⇔ (Underscript[ϵ, R])[
                              x]}, {(Underscript[0, N]) = (Underscript[0, R])}, {(Underscript[1, N]) = (Underscript[1, R])}, {\(x\( + \+N\)y = x\( + \+R\)y\)}, {\(\(-\+N x\) = \(-\+R x\)\)}, {\(x\( - \+N\)y = x\( - \+R\)y\)}, {\(x\(*\+N\)y = x\(*\+R\)y\)}, {\(x\( > \+N\)y ⇔ 
                            x\( > \+R\)y\)}, {(Underscript[rdm, N])[x, y]    = (Underscript[rdm, R])[x, y]}, {(Underscript[lcrd, N])[x, y]   = 
                            (Underscript[lcrd, R])[x, 
                              y]


                          }, {\(rd\+N[x, y]\ \  = 
                            x\( - \+N\)\(\(rdm\+N[x, 
                                  y]\(*\+N\)y\)\(
\)
                              \)\)}, {(Underscript[( trd), N])[x, Y]   =(Underscript[trd, N])[x, Y, 1] }, {(Underscript[trd, N])[x, Y, k]     =
{({{x, ⇐, k > \[LeftBracketingBar]Y\[RightBracketingBar]}, {where[x1 = (Underscript[rd, N])[x, (Subscript[Y, k])],
{({{(Underscript[trd, N])[x1, Y, 1], ⇐, \(x\( > \+N\)x1\)}, {(Underscript[trd, N])[x, Y, k + 1], ⇐, otherwise}})} ], ⇐, otherwise}})}
}, {\(\(cpd\+N[x, y]\  (*\ 
                              the\ critical\ pair\ difference\ of\ x\ and\ y\ *)  = 
where[lxy = lcrd\+N[x, y], 
                              rd\+N[lxy, x]\( - \+N\)rd\+N[lxy, 
                                  y]]\)\(\ \)\(
\)
                          \)}, {(Underscript[Gb, N])[X]    = (Underscript[Gb, N])[X, pairs[X]]}, {(Underscript[Gb, N])[
                              X, ⟨⟩] = 
                            X}, {\(Gb\+N[
                                X, ⟨⟨x, 
                                    y⟩, 
                                  p\&_⟩]\)=
where[h = (Underscript[trd, N])[(Underscript[cpd, N])[x, y], X],
{({{\(Gb\+N[
                                        X, ⟨p\&_⟩]\), ⇐, h = (Underscript[0, N])}, {\(Gb\+N[
                                        X⌢h, ⟨p\&_⟩ ≍ ⟨\(⟨X\_k, 
                                        h⟩\)\( \[VerticalSeparator] \+\(k = 
                                        1, …, \[LeftBracketingBar]X\[RightBracketingBar]\)\)⟩]\), ⇐, otherwise}})} ]
}, {(Underscript[rdGb, N])[X]     = (Underscript[ard, N])[(Underscript[Gb, N])[X]]}, {(Underscript[ard, N])[⟨⟩] = ⟨⟩}, {\(ard\+N[⟨p, 
                                q\&_⟩] = 
                            ard\+N[⟨⟩, 
                              p, ⟨q\&_⟩]\)}, {(Underscript[ard, N])[X, 
                              p, ⟨⟩]=where[h = (Underscript[trd, N])[p, X],
{({{X, ⇐, h = (Underscript[0, N])}, {X⌢p, ⇐, otherwise}})} ]}, {\(ard\+N[X, 
                              p, ⟨q, 
                                q\&_⟩]\)=where[\(h = 
                                  trd\+N[p, 
                                    X ≍ ⟨q, 
                                        q\&_⟩]\),
{({{\(ard\+N[X, 
                                        q, ⟨q\&_⟩]\), ⇐, h = (Underscript[0, N])}, {\(ard\+N[X⌢p, 
                                        q, ⟨q\&_⟩]\), ⇐, otherwise}})} ]}, {(Underscript[( tcrd), N])[x, Y]  (* 
                              the total cofactor reduction of x modulo tuple Y *)  = (Underscript[tcrd, N])[x, Y, 
                              1, ⟨(Underscript[0, N]) (Underscript[\[VerticalSeparator] , k = 
                                        1, …, \[LeftBracketingBar]Y\[RightBracketingBar]])⟩]}, {(Underscript[tcrd, N])[x, Y, k, C]     =
{({{⟨x, 
                                      C⟩, ⇐, k > \[LeftBracketingBar]Y\[RightBracketingBar]}, {where[c = (Underscript[rdm, N])[x, (Subscript[Y, k])],\(x1 = 
                                        x\( - \+N\)c\(*\+N\)Y\_k\),
{({{\(tcrd\+N[x1, Y, 1, 
                                        C\_\(k ⇤ C\_k\( + \+N\)c\)]\), ⇐, \(x\( > \+N\)x1\)}, {(Underscript[tcrd, N])[x, Y, k + 1, C], ⇐, otherwise}})} ], ⇐, otherwise}})}}})}})
	]]

Example

What should we do with this? We cannot really prove anything on an algorithm in this form? Nor can we apply it in this form to inputs.

Answer: Predicate logic contains a (good) programming language within itself. Let's program in predicate logic and execute these programs within logic. (This is the Theorema approach.)

Example

What should we do with this?

The Production of Formal Text

Needs formal training

Is not an obstacle for thinking but helps clarifying one's mind

\(The\ existence\ of\ formal\ knowledge\ bases\ in\ globally\ accessible\ libraries\ will\ reduce\ the\ work\ of\ paper\ writing\)

Formal writing will make mathematics more reliable,  
    re–usable,  understandable,  beautiful,  
    and efficient

The translation of existing papers to formal papers cannot / should not be fully automated

As a matter of fact, much of the content of the current mathematical literature is redundant, incorrect, incomplete, ambiguous, hard to read, ... and, therefore, never used.

It neither pays off to formalize all this "knowledge" as it stands. Nor is it possible: informal "formulae" that are incorrect, incomplete or ambiguous cannot be made correct, complete, and unambiguous by "translation".

Rather, much of the available mathematical knowledge will have to be formalized by human mathematicians whose insight into the respective mathematical subjects is better than the insight of the authors.

However, this translation will be necessary and tools that support this translation partially will be essential

A project I will pursue in the Theorema Group: "Mathematical Knowledge Editor".

The MK Editor will make proposals for the formalized formulae and the human user of the system can

      decide which variant to take
      and can polish the best variant.

(Like a kanji editor!)

Ultimately, much of mathematical research will become just a game of re-structuring knowledge in a formal way

Conclusion

See the section headings above.