Algebraic Constructions Applied to Theories

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>