Mathematical Knowledge Editor:
A Research Plan

Bruno Buchberger
RISC (Research Institute for Symbolic Computation)
Johannes Kepler University, Linz, Austria
and
RICAM (Radon Institute for Computational and Applied Mathematics)
Austrian Academy of Science, Linz, Austria
bruno.buchberger@jku.at

Koji Nakagawa
Faculty of Mathematics, Kyushu University, Fukuoka, Japan
nakagawa@math.kyushu-u.ac.jp

Version 2004-09-05: Copyright Bruno Buchberger, Koji Nakagawa 2004.

Abstract

We describe a tool, "Mathematical Knowledge Editor", which will fill an important gap in current technology for Mathematical Knowledge Management: the translation of mathematical knowledge contained in computer-processable files like, for example, LaTeX files into fully formal mathematical knowledge in the frame of a logic language like, for example, predicate logic. We think that a completely automated translation of this type is neither possible nor desirable. However, future Mathematical Knowledge Management systems, under the guidance and with the interaction of the human user, should provide as much computer-support as is reasonably possible for this translation. 

In this paper, we first specify the task the Mathematical Knowledge Editor should fulfill in the frame of the overall objectives of Mathematical Knowledge Management. Then we sketch our ideas for the detailed functionality of this tool and their possible implementation. As a target language we take the Theorema version of predicate logic. However, any version of predicate logic, in particular versions expressed in recent mathematical knowledge formats like  Mizar, OMDoc, OpenMath, MathML,  would serve equally well. In fact, we propose to work in an environment in which the easy translation between these formats is available.

As a benchmark application, we propose and describe the build-up of a comprehensive formal knowledge base for Groebner bases theory. This will be a major component of the activities planned for the special semester on Groebner bases in 2006 being organized by the first author in the frame of the RICAM institute.

Acknowledgement: Sponsored by FWF (Österreichischer Fonds zur Förderung der Wissenschaftlichen Forschung; Austrian Science Foundation), Project SFB 1302 ("Theorema") of the SFB 13 ("Scientific Computing"), and by RICAM (Radon Institute for Computational and Applied Mathematics, Austrian Academy of Science, Linz). This paper was written while the first author was a visiting professor at Kyoto University, Graduate School of Informatics (Professor Masahiko Sato) and, partly, during a research stay at Kyushu University, Faculty of Mathematics (Professor Kazuhiro Yokoyama) in summer 2004.

Nakagawa is (partially) supported by Kyushu University 21st Century COE Program, Development of  Dynamic Mathematics with High Functionality, of the Ministry of Education, Culture, Sports, Science and Technology of Japan.

The Goal of the Mathematical Knowledge Editor in the Frame of Mathematical Knowledge Management

Scenarios for Mathematical Knowledge Editing

Mathematical Knowledge Management (MKM) is a recent global effort to computer-support the entire process of generating and managing mathematical knowledge, see the proceedings of the respective conferences [MKM 2003a], [MKM 2003b], [MKM 2004].  The essential "reasoning" tools for MKM, like formulae simplifiers, proof checkers, logical decision algorithms, proof generators, algorithm verifiers, algorithm synthesizers, formulae retrievers, etc. work on mathematical knowledge bases that consist of mathematical formulae expressed in a formal mathematical language like predicate logic

Hence, before the reasoning tools of current and future MKM systems can be used for generating, verifying, re-arranging, and accessing (large) mathematical knowledge bases, initial mathematical knowledge must be expressed in predicate logic. For this, one may envisage two scenarios:

Input from scratch: In this scenario, the user would formulate the required formulae (definitions, propositions, problem specifications, algorithms, etc.) in predicate logic and type in these formulae by hand.

Translate existing documents: In this scenario, an existing mathematical text (e.g. a paper) in computer-readable form (e.g. a LaTeX) file would be taken as an input and an automatic translator would extract the formal mathematical content of the paper and translate it into the required (predicate) logic format.

Some people believe that the "input from scratch" scenario is unpractical because "it will never be possible to re-type all the useful mathematical knowledge contained in the current mathematical literature, which is mostly not written in a formal language like predicate logic". Other people believe that the "translate existing documents" scenario is unrealistic, because "it would need very intelligent tools to extract the intelligence contained in informal mathematical texts and express it in a formal language". Our own position is somewhat in between or, more precisely, is opposing both views. We think that, yes, the  "translate existing documents" scenario is unrealistic but not because informal mathematics can express things better than formal mathematics but mainly because most of the current mathematical papers have major deficiencies in terms of mathematical consistency, completeness, preciseness etc. that cannot be eliminated by just a "translation" into predicate logic. In other words, the mathematics contained in a mathematical paper cannot be improved by a translator even if such a translator would exist. Rather, most of the current mathematical papers will need a major interaction and assistance by a human mathematician in the process of being translated to predicate logic. On the other hand, yes, the "input from scratch" scenario is impractical because we would not really like to throw away all existing LaTeX files (e.g. of books on Groebern bases) and start to retype the whole stuff once again. However, to a certain extent, we believe that re-typing some of the mathematical texts in  predicate logic is  a practical and desirable option given the fact that, in the future, automated generation of (large) mathematical knowledge bases from small input by automated reasoners will be realistic and a routine tool. Also, in the long run, when MKM environments will become widely used, we envisage and propose that people write their mathematical papers in predicate logic  right from the outset so that a later translation will become superfluous.

Hence, the scenario we propose in this paper is as follows:

Interactive Translation: As target language for the translation we take (some version of) predicate logic because of its proven universal expressive power for mathematics.The input to the proposed Mathematical Knowledge Translator consists of source files containing mathematical knowledge in one of the current mathematical "representation languages" like LaTeX or PDF. The user sees a screen representation of these files, decides which parts he wants to "formalize" (translate into predicate logic) and the Mathematical Knowledge Translator proposes a predicate logic version of these parts. The resulting predicate logic formulae may still be far from the intended or desired form. Hence, the user will have to edit and polish the proposed formulae by hand. The Mathematical Knowledge Translator will give some technical help also in this final polishing step.

This scenario will be explained in more detail in the main part of this paper. Before we do this we would like to identify the exact role and place of this kind of interactive Mathematical Knowledge Translator in the overall frame of Mathematical Knowledge Management:

The Exact Position of Mathematical Knowledge Editing in Mathematical Knowledge Management

In [Buchberger, Piroi 2004] we proposed the following break-down of the field of Mathematical Knowledge Management (MKM):

I. Logical MKM Tools: These tools operate on completely formalized mathematical knowledge, e.g. in predicate logic, and produce completely formalized mathematical knowledge. Such tools are, for example, provers, proof-checkers, model checkers, expression simplifiers, proof simplifiers, algorithm verifiers, algorithm synthesizers etc. In the view of the Theorema project, the logical MKM tools form the essential kernel of future MKM systems.

II. Organizational MKM tools: These are tools that assist in managing informal and formal mathematical knowledge in various ways. In [Piroi, Nucherger 2004] we mentioned three groups of such tools:

IIa. Tools that translate mathematical knowledge in printed form (older books, journal articles etc. not available in LaTeX or any other mathematical presentation language) to LaTeX or any other mathematical presentation format.

IIb. Tools that translate mathematical knowledge in a mathematical presentation format like LaTeX or PDF into logic (e.g. predicate logic) form.

IIc. Tools that help managing huge collections of mathematical formulae (mathematical knowledge bases) by generating, maintaining, and modifying hierarchical structures in mathematical knowledge. For example, the "Label Management" tool described in [Piroi, Buchberger 2004] falls into this group of tools. (Note that certain tools for managing mathematical knowledge, like functors and categories, are themselves mathematical objects and fall under the group I. above.)

Based on the discussion in [Nakagawa, Namura, Suzuki 2004], for describing the translation process IIa. and IIb. in more detail, we propose the following five "levels of digitization" of mathematical knowledge:

Level 0: printed documents (non-digitized).

Level 1: bitmap image documents of printed materials (e.g. GIF, TIFF documents).

Level 2: layout structure documents (e.g. PS, PDF documents).

Level 3: presentationally formatted documents (e.g. HTML, MathML, \LaTeX documents).

Level 4: logical semantic based documents (e.g. Mathematica, Theorema, OMDOC, Mizar documents).

Level 0 is the level of undigitized documents. This is still the status of the vast majority of current mathematical knowlege.

A document in level 1 is a bitmap image. Typical formats of this level are TIFF and Bitmap. The translation from level 0 to level 1 is trivial. It just needs scanning.

A document in level 2 is a file that contains character codes with indication of their sizes and positions. PS and PDF are  formats of this kind. (Of course, PS or PDF can just consist of images. In our context, we do not consider such a document as a level 2 document.) The translation from level 1 to level 2 is difficult. By recent work of M. Suzuki and his group, see [Suzuki et al. 2003], it is now possible to recognize mathematical formulae in level 1 documents and generate the corresponding presentation of these formulae as a level 2 expression (for example as an XML expression).

A document in level 3 is a file that has structural information on the documents in terms of, e.g., separating mathematical formulae from narrative text, nested section structure, separating the body of the text from headings, author information etc. A tool for the translation from level 2 to level 3 that  identifies   all this structural information  in level 2 documents automatically is described in [Nakagawa, Nomura, Suzuki 2004]. The  presentational structural analysis of the  mathematical formulae contained in level 2 documents  and the generation of the corresponding MathML or LaTeX docuements of level 3  are part of the project of M. Suzuki, see [Suzuki et al. 2003].

A document in level 4 consists of clearly defined portions that contain mathematical formulae and other parts that may contain all kind of informal information (narrative text in natural language, structural information on the section hierarchy, etc.). The mathematical formulae must be syntactically correct w.r.t. to the chosen logical language and, more importantly, they obtain their semantics by the chosen logical language and the knowledge base in the frame of which they are used. These knowledge bases, again, must be collections of syntactically correct formulae in the same logic language. The translation of level 3 documents to level 4 documents is a challenging task because formuale described in presentation languages like LaTeX etc. do normally not contain all the information for unambiguous and complete parsing.  Also parts of a mathematical formula (e.g. assumptions and declarations about the use of variables) may be distributed over several portions of a level 3 text and the knowledge needed for giving semantics to level 3 formulae may be hidden. Also, as a matter of fact, many mathematical formulae in level 3 texts are plainly wrong both syntactically and semantically. As stated in the introduction, we believe that a fully automated translation from level 3 to level 4 formulae is neither feasible nor desirable. Rather, in this paper, we will describe an interactive tool, the "Mathematical Knowledge Editor" that may assist a human user to do translations between level 3 and level 4 texts as much as possible but leaves the main control of the process and subtle decisions to the user.

The target language of formula translation from level 3 to level 4 will be some universal logic language like predicate logic. Note, however, that in certain cicumstances, e.g. in texts that only describe algorithms, a sub-language of a full-fledged logic language, e.g.  a programming language like Mathematica, may suffice as the target language. For standardization, in this project, we confine ourselves to design and implement a Mathematical Knowledge Editor whose target language is the Theorema version of predicate logic a sublangugae of which is also a programming language, see [Buchberger et al. 2000]. We think that this is not a severe restriction because the translation between any version of predicate logic to any other version is simple compared to the translation process from level 3 to level 4. We are not aware of any other project that is attacking this translation task.

Current and Future Mathematical Knowledge Editing

In our view, a Mathematical Knowledge Editor will have a limited life-time but, nevertheless, will play a fundamental role  in the development of mathematics over the next decades: Currently, since most of the mathematical knowledge is still on level 0, 1, 2, or 3, the availabilty of a Mathematical Knowledge Editor is pressing. Even if mathematical knowledge editing cannot be fully automated, a Mathematical Knowledge Editor may drastically reduce the time for bringing current level 0-3 level mathematical knowledge to level 4. However, after all relevant mathematical knowledge will be available in mathematical knowledge bases on level 4, say in year 20xx, we think it will be customary and reasonable for all further mathematical knowledge to be expressed directed on level 4. Hence, from 20xx on, a Mathematical Knowledge Editor will not any more play an important role or, rather, it will play a different role which we will explain in more detail in the main part of this paper.

We present this strategical consideration in a diagram that illustrates the increase of levels in mathematical documents between now and the year 20xx:

Note however that  the translation of level 0-3 knowledge to level 4 without a Mathematical Knowledge Editor (i.e. purely manually) may take significantly longer or even so long that the mathematics community may get demotivated for undertaking the formalization and automation process of mathematics at all:

Of course, we do not pretend to be able to predict the numbers xx and yy but we think that yy would be significantly higher than xx.

Here is one more diagram that illustrates the details of the translation process from the current state of mathematical knowledge presentation, by partial translations 0->1, 1->2, 2->3, 3->4,  to the desired state in which all significant mathematical knowledge will be available in level 4 format:

This diagram emphasizes again the importance of the translation between level 3 and level 4. Whereas all the translation from levels 0-2 to level 3 is already covered by current technology, the translation between 3 and level 4 is not yet supported by any tools. It is the essential goal of the Mathematical Knowledge Editor specified in this paper.

Example: A Document in Level 0 - 4 Presentation

We randomly choose a paper in the area of Groebner bases theory, [Tran 2004] and show the realization of a small part of it in levels 0 - 4:

Level 0: Printed version.

Level 1, bitmap after scanning:

To be inserted. XXXX

Level 2, PDF format:

To be inserted. XXXX

Level 3, LaTeX format:

To be inserted. XXXX

Level 4, (Theorema) predicate logic format:

(Underscript[∀ , X,  < ])(is–admissible–order[
              X,  < ]⇔∧{({{is–total–order[𝕋[
                      X],  < ]}, {(Underscript[((Underscript[∀ , t ∈ 𝕋[X]])), t ≠ 1])1 < t}, {(Underscript[∀ , s, t, u ∈ 𝕋[X]])(s < t \[Implies] s *u < t *u)}})} )

Specification of the Mathematical Knowledge Editor

The Logical Target Language

In this paper, we choose the Theorema language, see e.g. [Buchberger et al. 2000], which is a version of predicate logic, as the target language into which all mathematical formulae should be translated. This is no restriction because the translation between various versions of predicate logic, e.g. the ones used in the various theorem proving systems like, for example, MIZAR and the recent mathematical formats like OMDOC, MathML, OpenMath etc. is a relatively easy task. In fact, in the Theorema system, there already exist a couple of translators between Theorema and other versions of predicate logic.

Input / Output Specification of the Mathematical Knowledge Editor

Input:

Any level 3 mathematical document (or collection of documents) D.

A formal knowlede base K (collection of formulae in the target logic language).

Output:

A level 4 document that contains

those formulae of D, translated to level 4,  which the users wants to be translated

in a translation that reflects the semantics of the formulae intended by the author of D
w.r.t. the formal knowledge base K

and an update of K that represents hidden knowledge in D that is necessary for conveying the semantics intended by the author of D

(together with non-mathematical information contained in D, i.e. information that, in Theorema / Mathematica notebooks would be stored in text cells, sections cells, reference lists etc.)

We think that this specification makes it clear how much of user interaction will normally be necessary for the translation of level 3 to level 4 documents: "intended semantics" and "hidden knowledge" in typical cases is something which only can be clarified and made explicit by an (experienced) human who guides the translation process.

For the discussion of the functionality of the Mathematical Knowledge Editor, we do not bother how the level 3 input  documents were created: They could have been typed by a mathematicians (e.g. as LaTeX documents), they also could have been produced by the tools available for translating level 0-2 documents to level 3 documents, e.g. the tools described in [Suzuki et al. 2003].

The Three Phases of Mathematical Knowledge Editing

>From the above rough specification of the Mathematical Knowledge Editor, it should be clear that mathematical knowledge editing naturally decomposes into three consecutive phases:

Identification: Identification of those parts of the level 3 document that contain mathematical knowledge (in level 3 presentation) and that should be translated to level 4 formal presentation. This identification will normally be done by the user. Alternatively, it may already have been done by the structure analysis tool described in [Nakagawa et al. 2004].

Formalization Proposals: For the mathematical formula parts identified in the identification phase, the Mathematical Knowledge Editor should propose one or several translations into level 4 formulae. This is the main and most challenging task of the editor. The more sophistication goes into this part, the easier the formalization task will become for the user.

Polishing: From the formalizations proposed by the Mathematical Knowledge Editor, the user will choose the one which comes closest to what he thinks is the intended meaning. Starting from this formula, the user will polish the formula by modifying certain parts of it. This polishing process should also be supported by the Mathematical Knowledge Editor by various expression editing tools like palettes etc.

Example

We take the following paragraph from[Tran...]

In the first phase we could, for example, identify the following formula

In the second phase, the Mathematical Knowledge Editor might propose the following formalizations:

Proposal 1:

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

Proposal 2:

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

Proposal 3:

We select the one which we think comes closest to the intended meaning, e.g. proposal 3

is–admissible–term–order⇔∧{({{is–total–order}, {1 = ((Subscript[x, 1])^0) . ((Subscript[x, 2])^0)  …((Subscript[x, n])^0)}, {\(∀ \+\(t ∈ \([X]\)\{1}\)1 < t\)}, {(Underscript[∀ , s, t, u ∈ [X]])(s < t \[Implies] 
                    s . u < t . u)}})}

Finally, we modify this to

(Underscript[∀ , X,  < ])(is–admissible–order[
              X,  < ]⇔∧{({{is–total–order[𝕋[
                      X],  < ]}, {(Underscript[((Underscript[∀ , t ∈ 𝕋[X]])), t ≠ 1])1 < t}, {(Underscript[∀ , s, t, u ∈ 𝕋[X]])(s < t \[Implies] s *u < t *u)}})} )

if we believe that this is the intended meaning relative to a knowledge base which would include already the definition of the set 𝕋[X] of all powerproduct over the set X of indeterminates, where 1 and * are already defined to be the unit and the multiplication in 𝕋[X] , respectively.

As one sees in this simple example, an automated formalization of the formula is not only difficult but, in a sense, impossible for various reasons:

The author does not explicitly state the ordering <, which is an important parameter in the definition. This parameter can only be guessed from the context by an experienced reader.

The quantifiers '∀' do not have an explicit scope. Their scope can only be guessed from the context. In this example, the guess is relatively easy because the formula in the original document has a line-by-line structure and it is probably clear that each of the quantifiers should extend over only one line.

The identification of 'X'  (rather than '[X]') as the actual free parameter in the definition of the binary predicate 'is–term–order' is subtle. In fact, according to the rules of predicate logic, 'X' should be used on the left-hand side of the definion but '[X]' should be used on the right-hand side. Since, however, angle brackets are used as structuring constructs for function and predicate application in (the Theorema version of) predicate logic, we have to change this to something different here like, for example,  '𝕋[X]' (for "the set of power products or terms generated by the indeterminates X").

The equality 1 = ((Subscript[x, 1])^0) . ((Subscript[x, 2])^0)  …((Subscript[x, n])^0) is actually a definition inside a definition. This is not appropriate because the definition of 1 for 𝕋[X] is not local to the definition of the notion of admissible order. Thus, the the definion of 1 should be eliminated here and, rather, put (in an appropriate form) somewhere earlier in the text (together with the definition of * on power products).

Also, one sees in this simple example that the translation process heavily depends on the knowledge base K which is already available: The definition will change in dependence on how the domain of power products and the operations on this set are defined. Also, if we decide to incorporate the formula identified in this paper into a given knowledge base on Groebner bases theory then we might first want to check wether an equivalent definition is already contained in the knowledge base and we might then decide not to include the new formula at all. Note that checking whether a given formula (or an equivalent formula) is already contained in a given knowledge base is, by itself, a non-trivial problem which, however, belongs to the purely logical branch of Mathematical  Knowledge Management (the branch I. in the above dichotomy of MKM).

Note that, in the approach proposed in this paper, the Mathematical Knowledge Editor (MKE) is only an auxiliary tools that just saves typing effort in the translation of level 3 documents to level 4 documents. The more sophistication we will be able to implement in the MKE, the more writing effort can be saved. However, the ultimate responsibility for the result of the formalization is always at the side of the user of the system.

The Flow of the Interaction Between the User and the Mathematical Knowledge Editor

In this section, we want to clarify and describe the formats on which the Mathematical Knowledge Editor (MKE) and the user work in the subtle interaction between the user and the MKE. Roughly, this can be illustrated by the following diagram:

The input formula is supposed to be available in a LaTeX file or a file in some other mathematical formulae representation language. This means that the formulae is just a linear string of ASCII characters describing the two-dimensional arrangement of the formula on a screen or in print.  (Note that this string, however, does not describe the logical structure of the formula!)

The user sees this formula on a window on his screen. He will study this formula and try to figure out the intended meaning.

The MKE produces a couple of proposals in (the Theorema version of) predicate logic. Internally, any Theorema predicate logic formula is just a nested Mathematica expression in linear ASCII representation.   (However, note that these expressions, in contrast to the LaTeX descriptions, completely describe the logical structure so that all kinds of algorithmic reasoners can work on these formulae!)

The Mathematica two-dimensional representation generator (together with a specific Mathematica program for producing the particular Theorema two-dimensional representation) automatically produces a two-dimensional representation of the formula on the screen.

The user can now work on this two-dimensional representation of the formula directly on the screen, i.e. he can modify this presentation interactively on the scree until he is satisfied.

The Mathematica / Theorema syntax system automatically does all these modifications also on the internal nested Mathematica expression level.

Thus, the user will be able to work exclusively on the two-dimensional formulae on the screen for producing the final formulae, while the system is providing the internal representations as  Mathematica nested expressions. The user need not bother about the internal representation.

In fact, the Mathematica / Theorema syntax system has an intermediate level between the nested Mathematica expression representation and the two-dimensional representation on screen, which is called the "nested boxes representation".

One can inspect the internal nested Mathematica expression form of a Theorema  (predicate logic) formula by the 'InputForm' command of Mathematica and the box format by using the Ctrl E key. For example, by putting the cursor into the input cell containing the following the Theorema formula

(Underscript[∀ , X,  < ])(is–admissible–order[
              X,  < ]⇔∧{({{is–total–order[𝕋[
                      X],  < ]}, {(Underscript[((Underscript[∀ , t ∈ 𝕋[X]])), t ≠ 1])1 < t}, {(Underscript[∀ , s, t, u ∈ 𝕋[X]])(s < t \[Implies] s *u < t *u)}})} )

we obtain the following box representation

Cell[BoxData[
    RowBox[{
      UnderscriptBox["∀", 
        RowBox[{"X", ",", "<"}]], 
      RowBox[{"(", 
        RowBox[{
          RowBox[{
            RowBox[{"is–admissible–order", "[", 
              RowBox[{"X", ",", "<"}], "]"}], "⇔"}], "∧", 
          RowBox[{
            StyleBox["{",
              SpanMaxSize->Infinity], GridBox[{
                {
                  RowBox[{"is–total–order", "[", 
                    RowBox[{
                      RowBox[{"𝕋", "[", "X", "]"}], ",", "<"}], "]"}]},
                {
                  RowBox[{
                    UnderscriptBox[
                      UnderscriptBox["∀", 
                        RowBox[{"t", "∈", 
                          RowBox[{"𝕋", "[", "X", "]"}]}]], 
                      RowBox[{"t", "≠", "1"}]], 
                    RowBox[{"1", "<", "t"}]}]},
                {
                  RowBox[{
                    UnderscriptBox["∀", 
                      RowBox[{"s", ",", "t", ",", 
                        RowBox[{"u", "∈", 
                          RowBox[{"𝕋", "[", "X", "]"}]}]}]], 
                    RowBox[{"(", 
                      RowBox[{
                        RowBox[{"s", "<", "t"}], "\[Implies]", 
                        RowBox[{
                          RowBox[{"s", " ", "*", "u"}], "<", 
                          RowBox[{"t", " ", "*", "u"}]}]}], ")"}]}]}
                },
              ColumnAlignments->{Left}], 
            StyleBox["}",
              ShowContents->False]}]}], " ", ")"}]}]], "Input"]

that describes, in an abstract form, the two-dimensional representation of this formula on the screen.  If (Theorema is loaded and) we apply the 'InputForm' command to the same input cell, we obtain the internal representation of this formula as a nested Mathematical expression:

•[(Underscript[∀ , X,  < ])(is–admissible–order[
                  X,  < ]⇔∧{({{is–total–order[𝕋[
                          X],  < ]}, {(Underscript[((Underscript[∀ , t ∈ 𝕋[X]])), t ≠ 1])1 < t}, {(Underscript[∀ , s, t, u ∈ 𝕋[X]])(s < t \[Implies] s *u < t *u)}})} )]// InputForm

™ForAll[•range[•simpleRange[•var[
            X]], •simpleRange[•var[™Less]]], 
      True, ™Iff[
        is–admissible–order[•var[
            X], •var[™Less]], ™And[
          is–total–order[𝕋[•var[
                X]], •var[™Less]], ™ForAll[•range[•setRange[•var[
                  t], 𝕋[•var[
                    X]]]], ™Not[™Equal[•var[t], 
                1]], •var[™Less][
              1, •var[
                t]]], ™ForAll[•range[•setRange[•var[s], 𝕋[•var[
                    X]]], •setRange[•var[
                  t], 𝕋[•var[
                    X]]], •setRange[•var[
                  u], 𝕋[•var[X]]]], 
            True, ™Implies[•var[™Less][•var[s], •var[
                  t]], •var[™Less][™Times[•var[s], •var[u]], ™Times[•var[
                    t], •var[u]]]]]]]]

(For technical reasons, which are not relevant for the purpose of this paper, we have to wrap the Theorema formula into •[...] before applying the InputForm command. This may be different in future versions of Theorema.)

Note also that, in Theorema, the translation between the internal nested expression representation of predicate logic formulae and the box representation (that describes, in a quite abstract way, the two-dimensional representation of the formulae on the screen) is user-programmable (by using certain tools of the the Mathematica front-end and programming language), i.e. the user has a high degree of freedom for designing and implementing his favorite 2-dimensional appearance of (predicate logic) formulae on the screen or in print while not changing the internal format of the formulae on which the algorithmic reasoners of the Theorema system work.

A Formal Knowledge Base for Groebner Bases Theory

The Strategic Goal of a Formal Knowledge Base for Groebner Bases Theory

We want to build up a formal knowledge base for Groebner bases theory, i.e. a knowledge base that consists of a well-structured, extensible and easily restructurable collection of all the definitions, propositions, problem specifications, and algorithms in Groebner bases theory formalized in (the Theorema version of) predicate logic. Depending on the logic tools available (in particular, the reasoning tools of Theorema), the knowledge base will also contain (automatically and manually generated) proofs of the propositions contained in knowledge base. In the long run, the knowledge base should cover the contents of all the books and research articles in Groebner bases theory and its applications.

Building up this knowledge base serves a couple of strategic goals:

The knowledge base should be accessible over the web and should facilitate future research, teaching and application activities in Groebner bases theory and related subjects.

The knowledge base should be a model and benchmark for future mathematical knowledge management and should challenge and improve the technology for all aspects of mathematical knowledge management.

Building up this knowledge base should be an important activity in the frame of the planned "Special Semester on Groebner Bases" organized jointly by RICAM (Radon Institute for Computational and Applied Mathematics, Austrian Academy of Science) and RISC (Research Institute for Symbolic Computation, Johannes Kepler University) in Linz / Hagenberg, Austria.

Building up this knowledge base also is well integrated into the Kyushu University 21st Century COE Program, Development of  Dynamic Mathematics with High Functionality, of the Ministry of Education, Culture, Sports, Science and Technology of Japan.

We hope that the project of building up a comprehensive formal knowledge base for Groebner bases theory will also find the cooperation of other research projects and groups throughout the world and we solicit the cooperation of all the researchers working in Groebner bases theory to contribute to this endeavor.

Facilitate Future Research, Teaching, and Application

Current research, teaching, and application of Groebner bases theory is mainly based on knowledge contained in  level 0-3 documents (books, articles, etc.) and on algorithm implementations in mathematical software systems like Mathematica, Maple, CoCoa, Singular, RISA / ASIR etc., which in our classification are level 4 documents in a limited target language (programming languages).  The algorithm implementations in mathematical software systems are, of course, important tools for current research (computational experiments), teaching, and application of Groebner bases theory. The vast information on Groebner bases theory contained in level 0-3 documents, however, is not accessible to computer-supported research, teaching, and application. Current algorithm implementations in the mathematical software systems do not even contain formal specifications of the problems solved by the algorithms nor any formal description of the complexity of the algorithms. Thus, no proofs (neither manual nor automated proofs) of properties of the algorithms can be based on these implementations. Also, conjectures motivated by computational experiments cannot readily be formally studied (verified or disproved). If an author wants to write a research paper or lecture notes, he does not get any support in composing the relevant prerequisite portion of Groebner bases theory and to apply current computer-supported reasoning technology for making his investigations more efficient, reliable, and comparable with the current research results in the field.

We envisage a future in which research, teaching, and application of Groebner bases theory is carried out in the environment of a fully formalized knowledge base that reflects the current level of research in the field and new research results are readily formally verified against the current knowledge and, if verified, are integrated into the knowledge base.

Model and Benchmark for Future Mathematical Knowledge Management

As pointed out in the initial section of this paper, Mathematical Knowledge Management (MKM) has two important aspects: Reasoning tools working on formal knowledge and organization, auxiliary tools. The development of sophisticated tools for both aspects will be challenged, motivated, and supported by the availability of large knowledge bases

Special Semester at RICAM

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

The preparatory phase will include the following activities:

–	definition of major emphasis topics of special semester and workshop subjects (co-organized by external scientists)

–	worldwide announcement of the special semester 

–	invitation of senior and junior visiting researchers, postdocs, graduates students 

–	build-up of web site and date base of web-accessible, downloadable papers

–	research for and set-up of the formalized knowledge base within the Theorema system

–	organizational steps towards establishing a global and long-term information center on Gröbner bases and related fields.

As can be seen from these steps, build-up of the formalized knowledge base on Groebner bases theory must seen in connection with building up a traditional data base of all the literature on Groebner bases with access to down-loadable literature items.

The special semester itself will consist of the following activities:

–	intensive courses and tutorials for young researchers, in particular postdocs and PhD students, and also mathematicians working in other fields

–	February 2006: “International Conference on Gröbner Bases and Related Theories” as research kick-off event for the special semester

–	1 – 6 months research stays of leading researchers in the field with thematic seminars

–	1 – 6 months research stays of junior researchers, postdoc researchers and PhD students

–	organization of special workshops during the semester

–	internal seminars

–	contributions of the visiting researchers and young researchers to the build-up of the papers data base and the formalized knowledge base

–	end of July 2006: Internal Workshop „Progress Report on Gröbner Bases and Related Theories“.

The follow-up phase will consist of the following activities:

–	running of the Information Center on Gröbner bases and related methods

–	preparation of the Conference 2007

–	fall 2007: International Conference on Gröbner Bases and Applications (in connection and coordination with Computer Algebra Application conferences and related conferences)

        -–	presentation of the scientific results of the special semester and the worldwide research stimulated by the special semester 

        -–	tutorials on the Gröbner bases method and related methods

        -–	tutorials on the applications of Gröbner bases and Gröbner bases software for the industry.

–	bi-annual conference on Gröbner bases and related methods starting from 2009.

The formalized knowledge base on Groebner bases theory will play an important role in the long-term effect of the special semester.

Kyushu University, 21st Century COE Program: Development of  Dynamic Mathematics with High Functionality

The build-up of a comprehensive formal knowledge base on Groebner bases theory can also be seen as an important benchmark example for "Dynamic Mathematics with High Functionality" as proposed in the respective project of the Faculty of Mathematics of Kyushu University. All of the central ideas of this project,

dynamism

high functionality

international cooperation

computational orientation

applicability in science and engineering

are reflected to a particularly high degree in our proposal for creating a formal knowledge base for Groebner basis theory:

Dynamism: Future formal knowledge bases should be dynamic in the sense that they should be easily extensible and restructurable.

High functionality: The formal reasoning tools applicable to formal knowledge bases allow a completely new degree of sophistication in their functionality, which cannot be compared with what is possible by current technologies (like semantic web technology) on conventional knowledge bases.

International cooperation: As explained in the other sections of this paper, the planned build-up of a formal knowledge base for Groebner bases theory is projected to be a nucleus for various other intitiatives, programs, and projects in the world that can dock to each other.

Computational orientation: Processing formal knowledge bases, which essentially is formal reasoning, is computation but computation on the meta-level of describing mathematical objects rather than on the level of computing with the mathematical objects.

Applicability in science and engineering: The availability of formal knowledge bases will make all kinds of applications of mathematical theories, like the theory of Groebner bases, more efficient, reliable, maintainable and exchangable.

Coordination with Other Projects in the World

The RICAM / RISC special semester and, in particular, the project of building up a formalized knowledge base for Groebner bases theory will seek the cooperation and coordination with other projects in this area, e.g.

School on Groebner Bases and Applications, 9-22 July 2005, IASBS, Zanjan, Iran, organized by Rashid Zaare-Nahandi.

The special year on Computational Methods in Algebraic Geometry at IMA, University of Minneapolis, USA.

Conclusion

We proposed a tool, the Mathematical Knowledge Editor, that supports the use to translate formulae in LateX (or any other formulae representation language) into corresponding formulae in the frame of a formal logic language, e.g. the Theorema version of predicate logic. This tool will be instrumental in the future translation of mathematical knowledge into a completely formalized form within (a version of) predicate logic. We explain why the complete formalization of mathematics is necessary for being able to use current and future algorithmic reasoning tools for processing mathematical knowledge.

We do not believe that complete automation of the translation of mathematical knowledge formulated in representation languages like LaTeX into formulae in a logic language will be possible and we give arguments for this. However, we do believe that a partial support of this translation  by a translation tool will be both feasible, desirable, and useful. We intend to implement such a tool in a sequence of levels of increasing sophistication. Higher sophistication will save time in the manual post-processing of the formulae that will lead to the final form of the knowledge to be stored in future formal mathematical knowledge bases.

References

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

[MIZAR] The MIZAR Project. www.mizar.org.

[MKM2003 a] 
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.
(Containing also the best papers of the 1st Conferences on Mathematical Knowledge Management, Sept.  ,  Research Institute of Symbolic Computation, Johannes Kepler University, Hagenberg, Austria.)

[MKM2003 b]  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.

[MKM 2004]
(eds.)
Proceedings of the Third International Conference on Mathematical Knowledge Management (MKM 2004), Bialowieza, Poland, September 19-21, LNCS 3119, Springer Heidelberg- Belin - New York, 2004.

[Nakagawa, Nomura, Suzuki 2004] K. Nakagawa, A. Nomura, and M. Suzuki.  
Extraction of Logical Structure from Articles in Mathematics. 
To appear in [MKM 2004].

[Piroi, Buchberger 2004] F. Piroi and B. Buchberger. 
An Environment for Building Mathematical Knowledge Libraries. 
In [MKM 2004]

[Suzuki et. al. 2003] M. Suzuki, F. Tamari, R. Fukuda, S. Uchida, and T. Kanahori. 
INFTY - An Integrated OCR System for Mathematical Documents. 
In: Proceedings of ACM Symposium on Document Engineering (DocEng '03), Grenoble,  France, Nov. 20-22, 2003. xxxxx