COmputational COmmutative Algebra

Villa Gualino, Torino, Italy
May 31 - June 5, 1999

Theorema: A New Kind of Mathematical Software System

Bruno Buchberger
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria

In the Theorema system, the user can

The emphasis of the system is on providing various automated provers. The proofs generated by these provers read like proofs generated by human mathematicians, i.e. they are sequences of formulae with intermediate "explanations" in natural language. The proofs are presented in hierarchical text cells that can be opened and closed so that proof details can be shown or not according to the taste of the reader.

The system is implemented in Mathematica 3.0 and uses, in particular, the advanced front-end facility of this system.

In the talk we will give various examples that will

Theorema reflects the personal view and experience of the speaker on mathematical research and education and is currently under development by a working group at RISC directed by the speaker.