Modular Construction

  The library provides the foundation for relating logics, and the next step is to provide a well-known, usable mechanism for lifting the formal knowledge into standard practice. The model we are proposing is based on a lightweight module system that organizes the logical library. Modules have long been used for organizing software, and they are grounded in long standing methods of organization in mathematics, such as those used in abstract algebra [3].

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:

=0in=0in
• developing common presentations of knowledge that relate results in a common language,
• isolating logics so that unverified results cannot leak between theories,
• partitioning theories, so that relations can be made on supertheories,
• providing a formal framework for incrementally expressing and developing the relations themselves,
• automatically inheriting results in a theory to all its subtheories.

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.