The Theorema Project

Our project aims to close the gap between computing and proving by adding proving support to an existing [commercial] computer algebra system (Mathematica). A similar approach is pursued by few other research groups: Isabelle [Paulson:96], Analytica [Clarke-Zhao:93], NQTHM [Boyer:88a], Nuprl [Constable:86], Coq [Huet_all:94], HOL [Gordon:93], Oyster-Clam [Horn:88], [vanHermelen:89], Redlog [Dolzmann_Sturm:96].

The distinctive features of Theorema are:
- integration of an existing rewrite rule language (Mathematica) into our logic;
- imitation of human proof style;
- natural language formulation of proofs;
- combination of functor style programming with proving;
- integration of proving into math textbooks generation and interactive math teaching;
- multi-style proving triggered by special context.

The {\Theorema} system is being built up in the following layers:
- A mathematical language as a common frame for both non-algorithmic and algorithmic mathematics. The syntax of this language is implemented by using the syntax extension facilities of Mathematica and it allows to write logic formulae (theorems) containg executable parts (function definitions using induction and bounded quantifiers).
-The concept of "functor'' as the general mechanism for building up towers of mathematical domains, which allows the user to construct mathematical models.
- A general predicate logic prover of a ``natural style'' introduced in earlier papers by Buchberger (see e.g. [Buchb-Licht:81]).
- Various special theorem provers (and / or interactive proof developers) corresponding, in a natural way, to the various functors that build up mathematical domains. All these provers produce proofs that imitate the proof style of human mathematicians. By now, an induction prover for the natural numbers and one over the domain of lists over a given domain are already implemented, a prover for the domain of multivariate polynomials over a given domain of monomials is under way.
- A general facility that allows the presentation of proofs in the form of ``nested cells'', which is crucial for being able to read complicated proofs without losing the overview. This facility is based on the facilities for manipulating cells in Mathematica notebooks and can be automatically translated in HTML collections with similar functionality. (This paper is also produced in this way.)

For a more detailed description of the components, as well as of the theoretical and algorithmical background of the project, the reader is reffered to [Buchb-et-al:97] and [Buchb-Vasaru:97]. In this paper we discuss mainly the features of the software which are most relevant for education and training, together with few examples of proofs.