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.

• Type: Conference
• Year: 2009
• Where: MKM
• Authors: Robert Lamar, Fairouz Kamareddine, J. B. Wells
• Keywords: Document, Human-friendly Natural Language, Information Management, MKM 2009, Varied Computerised Forms