Show simple item record

dc.contributor.authorLamar, Robert
dc.date.accessioned2012-03-20T09:57:15Z
dc.date.available2012-03-20T09:57:15Z
dc.date.issued2011-05
dc.identifier.urihttp://hdl.handle.net/10399/2427
dc.description.abstractThis dissertation describes certain developments in computer techniques formanagingmathematical knowledge. Computers currently assistmathematicians in presenting and archiving mathematics, as well as performing calculation and verification tasks. MathLang is a framework for computerising mathematical documents which features new approaches to these issues. In this dissertation, several extensions to MathLang are described: 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 (Isabelle is the system we choose). The rules for translation are further discussed 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 skeleton framework to be used as a starting point for a formal document.en_US
dc.language.isoenen_US
dc.publisherHeriot-Watt Universityen_US
dc.publisherMathematical and Computer Scienceen_US
dc.rightsAll items in ROS are protected by the Creative Commons copyright license (http://creativecommons.org/licenses/by-nc-nd/2.5/scotland/), with some rights reserved.
dc.titleA partial translation path from MathLang to Isabelleen_US
dc.typeThesisen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record