Organized by RICAM (Radon Institute for Computational and Applied Mathematics)
in close cooperation with RISC (Research Institute for Symbolic Computation).
Directed by Bruno Buchberger (RISC and RICAM) and Heinz Engl (RICAM).

Workshop C: Formal Groebner Bases Theory

Date: March 06 - March 10
Chairman: Bruno Buchberger

The Objectives of the Workshop: A Personal View

Formal Mathematics, Mathematical Knowledge Management, Computer-Supported Mathematical Theory Exploration are various names for an emerging new field of symbolic computation that aims at computer-supporting ("automating", "mechanizing", "systematizing", ...) the process of inventing and verifying mathematical knowledge. Important phases and aspects of this process are:
  • the invention of mathematical definitions and axioms,
  • the invention of mathematical propositions and their proof (or dis-proof),
  • the invention of mathematical problems,
  • the invention of algorithms (methods, ...) for solving the problems
  • the collection of mathematical definitions, propositions, problems, and methods in well-structured, re-usable, expandable, restructurable knowledge bases and the logic-driven access of these knowledge bases (over the web)

Motivated by my desire to write a book on Groebner bases theory, in 1995, I found that a systematic development of a mathematical theory, in the computer age, should be supported by a (logic and software) system that does a significant part of the reasoning involved in the exploration of the theory automatically and lets the author concentrate on essential ideas, on the lay-out of the theory, on the design of the hierarchy of knowledge layers, and on the really difficult parts of the theory that need significant creativity and insight, etc. This was the beginning of my designing the Theorema system (which consumed so much of my time that, still, I did not write a book on Groebner bases!)

In the meantime, significant progress on the design and implementation of systems for supporting mathematical theory exploration has been made by various groups in the world (MIZAR, NuPrL, Izabelle, ..., Theorema). However, so far, hardly any case study in computer-supported mathematical theory exploration is convincing enough for attracting the attention of working mathematicians or letting them switch to a computer-supported style in their daily practice of mathematical theory exploration.

In the special case of Groebner bases theory, a few groups in the world have managed to automate some of the steps in the development of the theory. Notably, some groups are providing reasoning tools for the theory of polynomials, others managed to prove parts of the theory automatically, others started to work on the automated synthesis of my algorithm for computing Groebner bases. (I found a method for achieving this, called "lazy thinking", myself in the recent past.)

The workshop on "Formal Groebner Bases Theory" should bring together researchers who are active in the design and implementation of formal mathematics systems and their foundation and who have done or at least tried to do or plan to do applications of their systems for the formal exploration of Groebner bases theory.

I expect that, through the workshop, we will get insight of two different kinds:
  • Insight into the current capabilities of reasoning systems for the systematic exploration of entire mathematical theories.
  • Insight into the essential ingredients of Groebner bases theory (possible axiomatizations, generalizations, etc.) and the build-up of a formal knowledge base for Groebner bases theory.
  • Insight into the role of formal knowledge bases for the future of mathematics.

(I apologize that, in this workshop, I will assign myself quite a few time slots for lectures. The reason is that I consider this workshop also as a kind of tutorial for the doc and postdoc students participating in the special semester and, by a series of lectures during Workshop C, I will compensate for the fact that I devoted too little time to the doc and postdoc students during the previous workshops.)

Bruno Buchberger
(Chairman of Workshop C)

Monday, March 6th
09.30-09.50B. BuchbergerKick-Off: Salutatory
10.00-12.00B. BuchbergerThe Objectives of Formal Mathematics and the Objectives of the Workshop of Formal Gröbner Bases Theory
12.00-13.00B. Buchberger, W. WindsteigerIntroduction to Theorema: An Example of a Formal Math System
15.00-16.00B. BuchbergerAutomated Synthesis of a Groebner Bases Algorithm: An Exercise in Automated Algorithm Synthesis
16.00-16.45A. CraciunAn Implementation of Groebner Synthesis in Theorema

Tuesday, March 7th
09.00-10.00R. McCaslandA System for Mathematical Theorem Invention
10.30-11.30L. ThéryAutomated Proof of Buchberger's Algorithm in Coq
12.00-13.00J.L. Ruiz ReinaAutomated Proof of Buchberger's Algorithm in ACL2
14.30-15.30D. RatiuTowards Gröbner Bases Synthesis by Means of Proof Transformation
16.00-17.00J. RobuTheorem Invention and Verification in Geometry
17.30-18.45F. PiroiOrganizational Tools for Formal Mathematics in Theorema tar.gz

Wednesday, March 8th
09.00-10.00M. GiesePractical Reflection for Formal Mathematics in Theorema
10.30-11.30S. MechvelianiContinuing with the Algebraization of Logic
11.30-12.00S. RajaeeNon-associative Groebner Bases
12.00-13.00T. KutsiaEquational Reasoning in Theorema
17.00-18.00P. PauleThe NIST Project and its Relation to Formal Mathematics
~18.30Shuttle service
~19.00Heurigenhof Spatzenbauer

Thursday, March 9th
10.00-open endB. BuchbergerDiscussion: Knowledge Managment
14.00-15.00L. HellströmRewriting in PROPs

Friday, March 10th
10.00-open endB. Buchberger, H. Hong, P. Paule, A. SevensterMini-Workshop on a Formal Knowledge Base for the Journal of Symbolic Computation

Other discussions and seminars on research topics, research plans and possible joint projects (involving also the doc and postdoc students) will be defined and organized for Thu afternoon and Friday, March 10, as a consequence and follow-up of the lectures on Mo, Tue, We, and Thu.
Information | Application | Program | Location | Bibliography | Knowledge | Service | Links Webmaster