Please use this identifier to cite or link to this item:
|Title:||DEVELOPMENT OF A PORTION OF A THEORY LIBRARY FOR MECHANIZED MATHEMATICS SYSTEMS|
|Advisor:||Farmer, William M|
|Department:||Computing and Software|
|Keywords:||Computational Engineering;Computer Engineering;Software Engineering;Computational Engineering|
|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>|
|Appears in Collections:||Open Access Dissertations and Theses|
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.