Formalizations in Theorema 2.0

General Information

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.

List of Formalizations

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.

Installation

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:

1. Download the respective zip-file from the links above, and unzip it.
2. Store the notebook-files (.nb) contained in the zip-file anywhere in your file system.
3. 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.
4. If there are further files and/or folders, one of them is a README-file. Carefully read it and follow the instructions.
5. 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!

How to View Notebooks and Proofs

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.