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.