
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, ComputerSupported Mathematical Theory Exploration are various names for an emerging new field of symbolic computation that aims at computersupporting ("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 disproof),
 the invention of mathematical problems,
 the invention of algorithms (methods, ...) for solving the problems
 the collection of mathematical definitions, propositions, problems, and methods in wellstructured, reusable, expandable, restructurable knowledge bases and the logicdriven 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 layout 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 computersupported mathematical theory exploration is convincing enough for attracting the attention of working mathematicians or letting them switch to a computersupported 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 buildup 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.3009.50   B. Buchberger   KickOff: Salutatory 
10.0012.00   B. Buchberger   The Objectives of Formal Mathematics and the Objectives of the Workshop of Formal Gröbner Bases Theory


12.0013.00   B. Buchberger, W. Windsteiger   Introduction to Theorema: An Example of a Formal Math System 

15.0016.00   B. Buchberger   Automated Synthesis of a Groebner Bases Algorithm: An Exercise in Automated Algorithm Synthesis



16.0016.45   A. Craciun   An Implementation of Groebner Synthesis in Theorema 
Tuesday, March 7th 

09.0010.00   R. McCasland   A System for Mathematical Theorem Invention 
10.3011.30   L. Théry   Automated Proof of Buchberger's Algorithm in Coq


12.0013.00   J.L. Ruiz Reina   Automated Proof of Buchberger's Algorithm in ACL2
 

14.3015.30   D. Ratiu   Towards Gröbner Bases Synthesis by Means of Proof Transformation 
16.0017.00   J. Robu   Theorem Invention and Verification in Geometry 
17.3018.45   F. Piroi   Organizational Tools for Formal Mathematics in Theorema
 tar.gz

Wednesday, March 8th 

09.0010.00   M. Giese   Practical Reflection for Formal Mathematics in Theorema



10.3011.30   S. Mechveliani   Continuing with the Algebraization of Logic


11.3012.00   S. Rajaee   Nonassociative Groebner Bases


12.0013.00   T. Kutsia   Equational Reasoning in Theorema




17.0018.00   P. Paule   The NIST Project and its Relation to Formal Mathematics 
~18.30   Shuttle service 
~19.00   Heurigenhof Spatzenbauer 
Thursday, March 9th 

10.00open end   B. Buchberger   Discussion: Knowledge Managment 


14.0015.00   L. Hellström   Rewriting in PROPs


Friday, March 10th 

10.00open end   B. Buchberger, H. Hong, P. Paule, A. Sevenster   MiniWorkshop 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 followup of the lectures on Mo, Tue, We, and Thu.

