MathLang translation to isabelle syntax

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationIntelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings
Pages373-388
Number of pages16
Volume5625 LNAI
DOIs
Publication statusPublished - 2009
Event16th 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 - Grand Bend, ON, Canada
Duration: 6 Jul 200912 Jul 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5625 LNAI
ISSN (Print)0302-9743

Conference

Conference16th 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
CountryCanada
CityGrand Bend, ON
Period6/07/0912/07/09

Fingerprint

Isabelle
Syntax
Mathematics
Translating
Language
Natural Language
Mathematicians

Cite this

Lamar, R., Kamareddine, F., & Wells, J. B. (2009). MathLang translation to isabelle syntax. In Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings (Vol. 5625 LNAI, pp. 373-388). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5625 LNAI). https://doi.org/10.1007/978-3-642-02614-0_30
Lamar, Robert ; Kamareddine, Fairouz ; Wells, J. B. / MathLang translation to isabelle syntax. Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. Vol. 5625 LNAI 2009. pp. 373-388 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{127bc365df464764939735af847e3e00,
title = "MathLang translation to isabelle syntax",
abstract = "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. {\circledC} 2009 Springer-Verlag Berlin Heidelberg.",
author = "Robert Lamar and Fairouz Kamareddine and Wells, {J. B.}",
year = "2009",
doi = "10.1007/978-3-642-02614-0_30",
language = "English",
isbn = "3642026133",
volume = "5625 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "373--388",
booktitle = "Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings",

}

Lamar, R, Kamareddine, F & Wells, JB 2009, MathLang translation to isabelle syntax. in Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. vol. 5625 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5625 LNAI, pp. 373-388, 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, Grand Bend, ON, Canada, 6/07/09. https://doi.org/10.1007/978-3-642-02614-0_30

MathLang translation to isabelle syntax. / Lamar, Robert; Kamareddine, Fairouz; Wells, J. B.

Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. Vol. 5625 LNAI 2009. p. 373-388 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5625 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

ER -

Lamar R, Kamareddine F, Wells JB. MathLang translation to isabelle syntax. In Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. Vol. 5625 LNAI. 2009. p. 373-388. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02614-0_30