Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/9876
Title: | Algebraic Constructions Applied to Theories |
Authors: | Tran, Minh Quang |
Advisor: | Farmer, William M. Jacques Carette, Jeffery Zucker Jacques Carette, Jeffery Zucker |
Department: | Computing and Software |
Keywords: | MathScheme;library of formalized mathematics;algebraic constructions;the little theories method;biform theories;Other Computer Engineering;Other Computer Engineering |
Publication Date: | Oct-2011 |
Abstract: | <p>MathScheme is a long-range research project being conducted at McMaster University with the aim to develop a mechanized mathematics system in which formal deduction and symbolic computation are integrated from the lowest level. The novel notion of a biform theory that is a combination of an axiomatic theory and an algorithmic theory is used to integrate formal deduction and symbolic computation into a uniform theory. A major focus of the project has currently been on building a library of formalized mathematics called the MathScheme Library. The MathScheme Library is based on the little theories method in which a portion of mathematical knowledge is represented as a network of biform theories interconnected via theory morphisms. In this thesis, we describe a systematic explanation of the underlying techniques which have been used for the construction of the MathScheme Library. Then we describe several algebraic constructions that can derive new useful machinery by leveraging the information extracted from a theory. For instance, we show a construction that can reify the term algebra of a (possibly multi-sorted) theory as an inductive data type.</p> |
URI: | http://hdl.handle.net/11375/9876 |
Identifier: | opendissertations/4959 5940 2071504 |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
fulltext.pdf | 555.37 kB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.