Top-level context.
The database covers currently a greater part of the first 1400 theorems of the set.mm file by Norman Megill, splitted into several 'modules'. The following diagram lists the dependencies between these modules; solid line means the axioms and theorems of the referred module are assumed ('imported'); dotted line means that an interpretation for the axioms is provided and the theorems are used ('exported'). For example, the general transitivity theorems in equiv are used in equ for the equality relation between sets.
| Name | Comment |
| equ | Equality and Substitution |
| equ-ax | Axioms for equality and substitution. |
| equiv | Equivalence relations. |
| equiv-ax | Axioms for equivalence relations |
| extent | Extensionality |
| extent-ax | Axiom of Extensionality |
| order | Partial order relations |
| order-ax | Axioms for partial order relations |
| pred | Pure predicate calculus. |
| pred-ax | Axioms for predicate calculus. |
| prop | Propositional Calculus. |
| prop-ax | Axioms and definitions for propositional calculus. |
| set-extent-ax | Axiom of Extensionality (for sets) |
| unique | Exists unique, exists at most one |