×

Restoring natural language as a computerised mathematics input method. (English) Zbl 1202.68383

Kauers, Manuel (ed.) et al., Towards mechanized mathematical assistants. 14th symposium, Calculemus 2007, 6th international conference, MKM 2007, Hagenberg, Austria, June 27–30, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73083-5/pbk). Lecture Notes in Computer Science 4573. Lecture Notes in Artificial Intelligence, 280-295 (2007).
Summary: Methods for computerised mathematics have found little appeal among mathematicians because they call for additional skills which are not available to the typical mathematician. We herein propose to reconcile computerised mathematics to mathematicians by restoring natural language as the primary medium for mathematical authoring. Our method associates portions of text with grammatical argumentation roles and computerises the informal mathematical style of the mathematician. Typical abbreviations like the aggregation of equations \(a = b > c\), are not usually accepted as input to computerised languages. We propose specific annotations to explicate the morphology of such natural language style, to accept input in this style, and to expand this input in the computer to obtain the intended representation (i.e., \(a = b\) and \(b > c\)). We have named this method syntax souring in contrast to the usual syntax sugaring. All results have been implemented in a prototype editor developed on top of TEX\(_{\text{MACS}}\) as a GUI for the core grammatical aspect of MathLang, a framework developed by the ULTRA group to computerise and formalise mathematics.
For the entire collection see [Zbl 1119.68011].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T50 Natural language processing
68U15 Computing methodologies for text processing; mathematical typography

Software:

Isar; Mizar
PDFBibTeX XMLCite
Full Text: DOI