TY - GEN
T1 - MathLang translation to isabelle syntax
AU - Lamar, Robert
AU - Kamareddine, Fairouz
AU - Wells, J. B.
PY - 2009
Y1 - 2009
N2 - 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. © 2009 Springer-Verlag Berlin Heidelberg.
AB - 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. © 2009 Springer-Verlag Berlin Heidelberg.
UR - http://www.scopus.com/inward/record.url?scp=69149101889&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-02614-0_30
DO - 10.1007/978-3-642-02614-0_30
M3 - Conference contribution
SN - 3642026133
SN - 9783642026133
VL - 5625 LNAI
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 373
EP - 388
BT - Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings
T2 - 16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009
Y2 - 6 July 2009 through 12 July 2009
ER -