The modules we use represent logics and theories (possibly from different systems), and the knowledge from different systems can be related by finding a relation between their modules. In the architecture we are proposing (Figure 1), the MathBus is used as a communication mechanism, and mathematical knowledge is stored in multiple shared libraries. The MathBus provides a standardized protocol for sharing mathematics at the syntactic level; the library maitains logical dependencies between the knowledge, and the logical environment collects the results of the library into modules that represent generic components of logical knowledge.
The problems that arise in the module system revolve around isolating
and managing theories and their components, including the following:
The modular environment we are proposing is called . The
environment is a framework for defining and relating mathematical
tools and domains, but it is itself independent of any particular
formal system. is light-weight in this sense: only the knowledge
that is needed for the task at hand is loaded into the system. The
resource requirements increase only as the problem size increases.