Overview of Theorema
The
Theorema project aims at
extending current computer algebra systems by facilities for supporting
mathematical proving. The present earlyprototype version of the
Theorema
software system is implemented in
Mathematica . The system consists
of a general higherorder predicate logic prover and a collection of special
provers that call each other depending on the particular proof situations.
The individual provers imitate the proof style of human mathematicians
and produce humanreadable proofs in natural language presented in nested
cells. The special provers are intimately connected with the functors that
build up the various mathematical domains.
The longterm goal of the project is to produce a complete system which
supports the mathematician in creating interactive textbooks, i.e. books
containing, besides the ordinary passive text, active text representing
algorithms
in executable format, as well as proofs which can be studied at
various levels of detail, and whose routine parts can be automatically
generated. This system will provide a uniform (logic and software) framework
in which a working mathematician, without leaving the system, can get computersupport
while looping through all phases of the mathematical problem solving cycle:

the phase of specifying a problem including the compilation of relevant
knowledge and the definition of new concepts (predicates, functions) and
auxiliary algorithms;

the phase of exploring a given problem and creating ideas and conjectures
by studying examples using the available knowledge and algorithms;

the phase of proving or disproving conjectures and thereby increasing
the relevant knowledge base;

the phase of programming, i.e. transforming useful new and provenly
correct mathematical knowledge into algorithms for solving the initial
problem;

the phase of writing up one's finding in interactive mathematical
documents.
Maintained by
Webmaster.
© Research Institute for Symbolic Computation.