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.