<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> / Master of Science (MSc)
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/9876 |
| Date | 10 1900 |
| Creators | Tran, Minh Quang |
| Contributors | Farmer, William M., Jacques Carette, Jeffery Zucker, Jacques Carette, Jeffery Zucker, Computing and Software |
| Source Sets | McMaster University |
| Detected Language | English |
| Type | thesis |
Page generated in 0.0016 seconds