RISC-Linz RISC-Linz Research Institute for Symbolic Computation  

The Theorema System (Version 2.0)

What Is Theorema 2.0?

Theorema 2.0 is a Mathematica package (a collection of packages, in fact) that provides a Mathematical Assistent System (MAS) inside of and based on Mathematica. A MAS supports the user in
  • formulating and structuring of mathematical knowledge,
  • proving mathematical statements,
  • formulating and executing mathematical algorithms,
  • performing computations,
  • etc.

When Should You be Interested in Theorema 2.0?

If you know the predecessor version Theorema 1.0.

Theorema 2.0 is the successor version, it is completely re-designed and re-implemented. While preserving the key features such as natural-style mathematical input and output of formulas, natural-style automated proofs, combination of proving and computing inside one system, etc., Theorema 2.0 comes with an improved user-interface centered around a graphical user interface (GUI) guiding the user through all phases of their work. More ...

If you write mathematical documents including proofs or algorithms.

Theorema 2.0 can help you in generating proofs fully automatically or interactively. The proofs generated by the system are structured like proofs done by a well-educated mathematician and can be displayed on the screen, printed out, or included into the document.
Theorema 2.0 allows you to express algorithms using the language of predicate logic or parts of the Mathematica programming language supporting procedural programming, most importantly various forms of loops. Moreover, the algorithms can be executed immediately without any translation to any other system or language. More ...

If you want to develop hierarchies of mathematical theories

Theorema 2.0 allows you to organize mathematical knowledge as hierarchies of interdependent theories. Once you define a mathematical concept through a formula (expressed in predicate logic), you can "try out" the definition immediately on small finite examples, whether the formula "behaves" as expected, i.e. whether the formula expresses what you wanted to express with it. Once the definitions are settled, you can continue and try to prove some properties of the newly defined entities. More ...

How Can You Use Theorema 2.0?

Theorema Licensing

Theorema 2.0 is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License (GPL) as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

Installing Theorema 2.0

Theorema 2.0 is a standard add-on package for Mathematica and it is distributed as an archive file in various formats (zip, tar, 7z, etc.), which can be downloaded from the Theorema homepage. Installation of the system requires nothing more than unpacking the archive and moving the directory "Theorema" into one of the locations for standard add-on packages.

Loading Theorema 2.0

Once the system is properly installed, it is then loaded into the current Mathematica session by executing the Mathematica command
Click for copyable input
Theorema 2.0 requires at least Mathematica version 8.

How Can You Work with Theorema 2.0

While the system is loading, you see a welcome window on the screen. After this, a new window called Theorema Commander opens and marks the completion of the loading process. You are ready to start off.
"Working in Theorema 2.0" means developing a Theorema session, i.e.
  • writing structured mathematical documents in Mathematica notebooks using one of the special Theorema stylesheets and
    • performing certain operations on parts of the notebook using actions supported by the Theorema Commander (e.g. prove a theorem)
    For a first introduction to what can be done in a Theorema session we suggest to follow the First Tour in Theorema 2.0.

How Can You Contribute to Theorema 2.0?

Theorema source code is available as a Git repository from GitHub. We assume basic knowledge on "git" for communicating contributions to the Theorema source code.
If you intend to implement changes or improvements to the Theorema system, we recommend to contact the Theorema Group in advance in order to coordinate possible modifications. When you want to contribute code to the system, you need to provide a git repository from which we can pull the modifications. We encourage to use GitHub, but this is not a must.
For programming Theorema code, we recommend to use the Wolfram Workbench. When cloning the git repository you get a local directory that serves as the base directory for a workbench-project. In the workbench, just import the project from that directory into the default workspace. Due to formatting issues with the resulting code, please refrain from editing programs in the Mathematica notebook frontend. Please read the programmers' guidelines before you start implementing.