Below, you can download the formalizations of mathematical theories in
Theorema 2.0, created by
Alexander Maletzky.
Each formalization consists of one or more *content notebooks* (which are actually
*Mathematica* notebooks),
together with a bunch of *proof files*.

Note that this site will be superseded by an official online repository of so-called *Theorema Knowledge Archives*
in the future.

Name | Short Description |
---|---|

Reduction Ring Theory | GrÃ¶bner bases and reduction rings, together with several elementary mathematical theories (sets, algebraic structures, numbers, tuples, ...). |

Complexity Analysis | Complexity analysis of Buchberger's algorithm in bivariate polynomial rings over fields, w.r.t. a graded term order. |

The minimal prerequisite for being able to inspect and use the formalizations is to have *Mathematica* (version 8 or newer)
and Theorema 2.0 installed on your computer.

Theorema 2.0 is completely free and even open-source. You can obtain it from the
official website, which also provides detailed
information on how to properly install it.

The installation of a formalization is fairly straight-forward. Just follow the steps below:

- Download the respective zip-file from the links above, and unzip it.
- Store the notebook-files (.nb) contained in the zip-file anywhere in your file system.
- Furthermore, the zip-file contains some folders having the same name as one of the notebook files. These folders must be stored
**in exactly the same directory**as the corresponding notebook. - If there are further files and/or folders, one of them is a README-file. Carefully read it and follow the instructions.
- Now, the files are properly installed. If you want to open a notebook, start Theorema and open the notebook by clicking on the
"Open"-button in the Theorema-Commander window.
**Do not open Theorema notebooks directly with***Mathematica*!

Once you opened a notebook in Theorema (as described above), you can simply browse through its contents. If you want to inspect the proof of a theorem, just click on the respective "Show Proof" link appearing somewhere below the theorem. After a few seconds, a separate notebook displaying the nicely-formatted proof should pop-up (if not, make sure that you really followed step 3 of the above installation guide).

If a formalization consists of more than one notebooks, one of them, called "Overview.nb", contains some general information about the formalization and its logical structure. Therefore, it is a good idea to have a look at this notebook first.

If you encounter any problems, do not hesitate to contact the author. Normally, the formalizations are maintained and updated to work with the latest version of Theorema.