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,
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
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
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.
