System Architecture

The major components of the Theorema system are reflected in the top-level directory structure of the Theorema installation. The directories "Documentation", "FrontEnd", and "Kernel" are standard directories expected to be present in every Mathematica package, they are required in order to guarantee smooth integration of Theorema into Mathematica, e.g. system documentation will be available through the Mathematica Documentation Center.

Implements computational semantics of the Theorema built-in language constructs, e.g. numbers, tuples, finite sets, logical connectives, quantifiers with finite ranges, etc.

Color definitions for GUI components and notebooks.

Implements the whole graphical user interface displayed in the Theorema commander.

Implements the mechanisms that allow setting up the system interface in different languages.

This directory and its subdirectories collect user-supplied mathematical theories.

Here are the definitions for formatting Theorema expressions, which can occur both in computations and outside of computations. The rest of the definitions for formatting expressions is in Syntax.m, see below.

This file is special, it is not a package for itself, it is a plain file, which is loaded twice during the system startup process. Once it is loaded inside the context Theorema`Language` and once it is loaded in the context Theorema`Computation`Language`, so that all definitions collected in Expressions.m are available in both contexts.

This package collects functions for manipulating Theorema expressions, e.g. substitution of free variables, converting universally quantified equalities into Mathematica rewrite rules, etc.

This package defines functions used for organizing the Theorema session, e.g. storing definitions and theorems, processing of global declarations, etc.

This package defines the syntax of the Theorema language, both for input (MakeExpression and related) and for output (MakeBoxes and related). Regarding output, only a fragment of the language is defined here, the rest is in Expressions.m, see above.

This packages defines the general proving mechanism and everything needed for it, e.g. the overall proof search procedure, datastructures for proof objects, inference rule handling, etc.

This is a special package on the top-level of the hierarchy. Its purpose is to collect all public symbols to be exported. All packages that use symbols from other packages need to include only this package in order to have all exported symbols available.

The Theorema system consists of a multitude of packages. In the standard package layout in Mathematica, every package has a "public context" corresponding to the filename path and a "private context" (typically the public context with "`Private`" appended). The public contexts contain the names of symbols that should be visible outside of the package, these symbols are exported and can be used in other packages, due to the standard setup that puts the public context into Mathematica's context path $ContextPath. All non-exported symbols are in the respective private contexts and cannot be used in other packages since the private context is not part of the context path.

In order to keep the context path within a reasonable size, we setup context differently. Not every package corresponds to a context in the context path. Instead, we provide several contexts for symbols that should be shared between different packages of the system. These contexts typically do not correspond to a file in the system, they rather correspond to directories, although this must not be considered a strict rule of any significance.

The Theorema system is designed in such a way that language-dependent portions of the implementation are grouped in well-defined places. In this way, we try to support the translation of the entire system into different languages.