COCOA VICOmputational COmmutative Algebra
Villa Gualino, Torino, Italy |

Bruno Buchberger

Research Institute for Symbolic Computation

Johannes Kepler University, Linz, Austria

In the Theorema system, the user can

- enter definitions, axioms, propositions, algorithms and other formal math text in a syntax, which is as close as possible to the "usual" syntax of every-day mathematics
- group these formal texts in hierarchies of "knowledge bases"
- evaluate, solve, and prove formulae using knowledge bases

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

- demonstrate the touch and feel of the system
- explain the logical proof techniques and the implementation techniques used
- and give an impression of how a system of this type will change they way we can do mathematical research and teach mathematics.