DEVELOPMENT OF A PORTION OF A THEORY LIBRARY FOR MECHANIZED MATHEMATICS SYSTEMS

Abstract

<p>A theory library for a mechanized mathematics system (MMS) is a collection of mathematical theories which serves as a database of mathematics. A powerful library plays a significant role in making an MMS useful. This thesis demonstrates some of the techniques needed for generating a large theory library for an MMS, that has capability of both computation and deduction, by developing a small portion of a theory library. In the theory library presented in this thesis, the module system Mei, a (lamda)-calculus style module system that supports higher-order functors, is employed to manage mathematical theories. Chiron, a logic derived from von-Neumann-Bernays-Godel set theory, is used as the underlying logic of the system, and biform theories, which can include both formulas and algorithms as axioms, are used to present mathematical theories. The theory library given in this thesis is based on the branch of mathematics called calculus.</p>