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.50	B. Buchberger	Kick-Off: Salutatory
10.00-12.00	B. Buchberger	The Objectives of Formal Mathematics and the Objectives of the Workshop of Formal Gröbner Bases Theory
12.00-13.00	B. Buchberger, W. Windsteiger	Introduction to Theorema: An Example of a Formal Math System

15.00-16.00	B. Buchberger	Automated Synthesis of a Groebner Bases Algorithm: An Exercise in Automated Algorithm Synthesis
16.00-16.45	A. Craciun	An Implementation of Groebner Synthesis in Theorema

Tuesday, March 7th

09.00-10.00	R. McCasland	A System for Mathematical Theorem Invention
10.30-11.30	L. Théry	Automated Proof of Buchberger's Algorithm in Coq
12.00-13.00	J.L. Ruiz Reina	Automated Proof of Buchberger's Algorithm in ACL2

14.30-15.30	D. Ratiu	Towards Gröbner Bases Synthesis by Means of Proof Transformation
16.00-17.00	J. Robu	Theorem Invention and Verification in Geometry
17.30-18.45	F. Piroi	Organizational Tools for Formal Mathematics in Theorema	tar.gz

Wednesday, March 8th

09.00-10.00	M. Giese	Practical Reflection for Formal Mathematics in Theorema
10.30-11.30	S. Mechveliani	Continuing with the Algebraization of Logic
11.30-12.00	S. Rajaee	Non-associative Groebner Bases
12.00-13.00	T. Kutsia	Equational Reasoning in Theorema


17.00-18.00	P. Paule	The NIST Project and its Relation to Formal Mathematics
~18.30	Shuttle service
~19.00	Heurigenhof Spatzenbauer

Thursday, March 9th

10.00-open end	B. Buchberger	Discussion: Knowledge Managment


14.00-15.00	L. Hellström	Rewriting in PROPs

Friday, March 10th

10.00-open end	B. Buchberger, H. Hong, P. Paule, A. Sevenster	Mini-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.

Webmaster