Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/8922
Title: | DEVELOPMENT OF A PORTION OF A THEORY LIBRARY FOR MECHANIZED MATHEMATICS SYSTEMS |
Authors: | ABBASI, MEHWISH |
Advisor: | Farmer, William M |
Department: | Computing and Software |
Keywords: | Computational Engineering;Computer Engineering;Software Engineering;Computational Engineering |
Publication Date: | Sep-2009 |
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> |
URI: | http://hdl.handle.net/11375/8922 |
Identifier: | opendissertations/4090 5109 2013051 |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
fulltext.pdf | 1.57 MB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.