MathLang Translation to Isabelle Syntax

10 years 2 months ago
MathLang Translation to Isabelle Syntax
Converting mathematical documents from a human-friendly natural language to a form that can be readily processed by computers is often a tedious, manual task. Translating between varied computerised forms is also a difficult problem. MathLang, a system of methods and representations for computerising mathematics, tries to make these tasks more tractable by breaking the translation down into manageable portions. This paper presents a method for creating rules to translate documents from MathLang’s internal representation of mathematics to documents in the language of the Isabelle proof assistant. It includes a set of example rules applicable for a particular document. The resulting documents are not completely verifiable by Isabelle, but they represent a point to which a mathematician may take a document without the involvement of an Isabelle expert.
Robert Lamar, Fairouz Kamareddine, J. B. Wells
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where MKM
Authors Robert Lamar, Fairouz Kamareddine, J. B. Wells
Comments (0)