##
Invited talk

#
The Theorema Project: An Overview

##
Bruno Buchberger

Research Institute for Symbolic Computation (RISC)

The Theorema Project aims at integrating proving support into computer
algebra systems. The emphasis is on proof generation for routine parts of
proofs, structured proof presentation in natural language, and smooth
interaction with the existing solving and computing facilities of computer
algebra systems. Our present system frame is Mathematica 3.0.

We will first give an overview on the Theorema Project and then present
more details about the following aspects of the system:

A predicate logic prover that imitates the proof style of humans (in
particular the proof style of the authors).

A couple of special provers for various "areas" of mathematics (at
present, for equalities over natural numbers, lists, and polynomials),
where an "area" is defined by a functor that generates the domains in the
area, that are currently being developed. The main tool is simplification
together with setting up the induction recursively over the universally
quantified variables.

Automatic generation of knowledge bases by using the information
contained in the functors.

Stuctured proof presentation in (technical) natural language by using the
nested cells feature of Mathematica.

Theory generation versus theorem proving.

The talk will be illustrated by demos.