CHIRON: MECHANIZING MATHEMATICS IN OCAML

Abstract

<p>Computer algebra systems such as Maple [2] and Mathematica [12] are good at symbolic computation, while theorem proving systems such as Coq [11] and pvs [9] 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>