Exploring Computer Mathematics with Theorema

Tudor Jebelean and the Theorema Group

RISC-Linz, Austria

The Theorema system is developed at RISC-Linz by the Theorema group, under the leadership of Bruno Buchberger.

The goal of the Theorema project is to provide computer support for all phases of the mathematical work: to prove theorems, use them for computations and experiments, conjecture new theorems, prove those, extract solution methods from them, apply them in other proofs, etc. The Theorema system offers these features in one coherent software package which is currently based on the rewrite engine of the computer algebra system Mathematica.

The particular features of the system include:

The tutorial will contain 4 parts of about 30 minutes each:

The presentation will be based on concrete live experiments with the Theorema system, with concrete examples from various elementary theories. The audience is not expected to have specific training in any particular area, let it be automatic reasoning, computer algebra, or program verification. A general graduate level of knowledge in mathematics and computer science should suffice, since the Theorema system addresses all mathematicians, computer scientists, and engineers.

Throughout the presentation, we will give particular emphasis to refining and explaining the research problems described in the companion document Research problems related to Theorema.

The support of the presentation will be distributed to the tutorial attendees in electronic format, together with a working copy of the Theorema system (machine code, 12 months user license). Interested participants will be invited to become alpha-testers of Theorema.