Please use this identifier to cite or link to this item:
|Title:||CHIRON: MECHANIZING MATHEMATICS IN OCAML|
|Department:||Computing and Software|
|Keywords:||Computer Engineering;Computer Sciences;Software Engineering;Computer Engineering|
|Abstract:||<p>Computer algebra systems such as Maple  and Mathematica  are good at symbolic computation, while theorem proving systems such as Coq  and pvs  are well-developed for creating formal proofs. However, people are searching for a mechanized mathematics system which can provide highly integrated symbolic computation and formal deduction capabilities at the same time.</p> <p>My work is to design and implement the basis for a mechanized mathematics system based on a formal framework, which was previously developed as part of the MathScheme project at McMaster University. The core idea of the framework consists of the notion of a biform theory, which is simultaneously an axiomatic theory and an algorithmic theory, providing a formal context for both deduction and computation.</p> <p>A mechanized mathematics system which utilizes biform theories to represent mathematics requires a logic in which biform theories can be expressed. Chiron, as a derivative of von-Neumann-Bernays-Gödel set theory, is the logic we choose for our MMS development. It is intended to be a practical, general-purpose logic for mechanizing mathematics and has a high level of both theoretical and practical expressivity compared to other logics such as Zermelo-Fraenkel (ZF) set theory and first-order logic (FOL).</p> <p>The thesis presents the first stage of the development of the MMS. In particular, the type system of the MMS has been fully established along with all necessary expression constructors for building typed Chiron expressions. Half of the work for formalizing biform theories in Chiron has been implemented by introducing the notion of name spaces, which is used for exporting the low level implementation of Chiron transformers. We have experimented with the Chiron representation for expressing the meaning formulas of Chiron transformers, in particular for boolean algebra and logical operators in the other half of the work.</p>|
|Appears in Collections:||Open Access Dissertations and Theses|
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.