A partial translation path from MathLang to Isabelle
Robert Lamar · 2011
thesis or use of any of the information contained in it must acknowledge this thesis as the source of the quotation or information. This dissertation describes certain developments in computer techniques for managingmathematical knowledge. Computers currently assist math-ematicians in presenting and archiving mathematics, as well as perform-ing calculation and verification tasks. MathLang is a framework for com-puterising mathematical documents which features new approaches to these issues. In this dissertation, several extensions to MathLang are de-scribed: a system and notation for annotating text; improved methods for annotating complex mathematical expressions; and a method for creating rules to translate document annotations. A typical MathLang work flow for document annotation and computerisation is demonstrated, showing how writing style can complicate the annotation process and how these may be resolved. This workflow is compared with the standard process for producing formal computer theories in a computer proof assistant (Is-abelle is the system we choose). The rules for translation are further dis-cussed as a way of producing text in the syntax of Isabelle (without a deep knowledge of the system), with possible use cases of providing a text which can be used either as an aid to learning Isabelle, or as a skele-ton framework to be used as a starting point for a formal document. i ii For my family both present and future