Towards semantic mathematical editing. (English) Zbl 1329.68277

Summary: Currently, there exists a big gap between formal computer-understandable mathematics and informal mathematics, as written by humans. When looking more closely, there are two important subproblems: making documents written by humans at least syntactically understandable for computers, and the formal verification of the actual mathematics in the documents. In this paper, we will focus on the first problem.{
}For the time being, most authors use \(\mathrm T_{\mathrm E}\mathrm X\), \(\mathrm {L}^{\mathrm A}\mathrm T_{\mathrm E}\mathrm X\), or one of its graphical front-ends in order to write documents with many mathematical formulas. In the past decade, we have developed an alternative wysiwyg system GNU \(\mathrm T_{\mathrm E}\mathrm X_{\mathrm{MACS}}\), which is not based on \(\mathrm T_{\mathrm E}\mathrm X\). All these systems are only adequate for visual typesetting and do not carry much semantics. Stated in the MathML jargon, they concentrate on presentation markup, not content markup.{
}In recent versions of \(\mathrm T_{\mathrm E}\mathrm X_{\mathrm{MACS}}\), we have started to integrate facilities for the semantic editing of formulas. In this paper, we will describe these facilities and expand on the underlying motivation and design choices.{
}To go short, we continue to allow the user to enter formulas in a visually oriented way. In the background, we continuously run a packrat parser, which attempts to convert (potentially incomplete) formulas into content markup. As long as all formulas remain sufficiently correct, the editor can then operate both on a visual or semantic level, independently of the low-level representation being used.{
}An important related topic, which will also be discussed at length, is the automatic correction of syntax errors in existing mathematical documents. In particular, the syntax corrector that we have implemented enables us to upgrade existing documents and test our parsing grammar on various books and papers from different sources. We will provide a detailed analysis of these experiments.


68U15 Computing methodologies for text processing; mathematical typography
68N99 Theory of software
68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
Full Text: DOI


[1] Arsac, O.; Dalmas, S.; Gaëtano, M., The design of a customizable component to display and edit formulas, (ACM Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, July 28-31, (1999)), 283-290
[2] Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano, User interaction with the matita proof assistant, J. Autom. Reason., 39, 2, 109-139, (2007) · Zbl 1132.68673
[3] Audebaud, Ph.; Rideau, L., Texmacs as authoring tool for formal developments, Electron. Notes Theor. Comput. Sci., 103, 27-48, (2004)
[4] Axiom, The axiom computer algebra system, (1971)
[5] Basu, S.; Pollack, R.; Roy, M. F., Algorithms in real algebraic geometry, Algorithms Comput. Math., vol. 10, (2003), Springer-Verlag Berlin, Heidelberg, New York
[6] Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in real algebraic geometry, Algorithms Comput. Math., vol. 10, (2006), Springer-Verlag
[7] Bertot, Yves, The ctcoq system: design and architecture, Form. Asp. Comput., 11, 3, 225-243, (1999)
[8] Borras, P.; Clement, D.; Despeyroux, Th.; Incerpi, J.; Kahn, G.; Lang, B.; Pascual, V., Centaur: the system, SIGSOFT Softw. Eng. Notes, 13, 5, 14-24, (1988)
[9] Braun, T.; Danielsson, H.; Ludwig, M.; Pechta, J.; Zenith, F., (2003), Kile: an integrated LaTeX environment
[10] de Bruijn, N. G., The mathematical language AUTOMATH, its usage, and some of its extensions, (Symposium on Automatic Demonstration, Versailles, December 1968, Lect. Notes Math., vol. 125, (1970), Springer-Verlag), 29-61
[11] Chou, E., (2010), Collected course material
[12] Coquand, T., The coq proof assistant, (1984)
[13] DeRemer, F., Practical LR(k) translators, (1969), Massachusetts Institute of Technology, PhD thesis
[14] Dooley, Samuel S., Coordinating mathematical content and presentation markup in interactive mathematical documents, (Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation, (1998)), 54-61 · Zbl 0918.68159
[15] Dooley, Samuel S., Editing mathematical content and presentation markup in interactive mathematical documents, (Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation, (2002)), 55-62 · Zbl 1072.68637
[16] van den Dries, L., Tame topology and O-minimal structures, Lond. Math. Soc. Lect. Note Ser., vol. 248, (1998), Cambridge University Press · Zbl 0953.03045
[17] Ettrich, M., The lyx document processor, (1995)
[18] Ford, Bryan, Packrat parsing: simple, powerful, lazy, linear time, (Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP ’02, (2002), ACM Press New York, NY, USA), 36-47 · Zbl 1322.68040
[19] Ford, B., Packrat parsing: a practical linear-time algorithm with backtracking, (September 2002), Massachusetts Institute of Technology, Master’s thesis
[20] FSF, Gnu bison, (1998)
[21] Grozin, A. G., Texmacs interfaces to maxima, mupad and reduce, (Gerdt, V. P., Proc. Int. Workshop Computer Algebra and Its Application to Physics, Dubna, (June 2001)), No. 11-2001-279 in JINR E5 149
[22] Grozin, A. G., Texmacs-maxima interface, (June 2005)
[23] van der Hoeven, J., Transseries and real differential algebra, Lect. Notes Math., vol. 1888, (2006), Springer-Verlag · Zbl 1128.12008
[24] van der Hoeven, J., Transséries et analyse complexe effective, (2007), Univ. d’Orsay, PhD thesis, Mémoire d’habilitation
[25] van der Hoeven, J., GNU texmacs, (1998)
[26] van der Hoeven, J., GNU texmacs: a free, structured, wysiwyg and technical text editor, (Filipo, Daniel, Le document au XXI-ième siècle, vols. 39-40, Actes du congrès GUTenberg, Metz, 14-17 mai 2001, (2001)), 39-50
[27] Johnson, S. C., Yacc: yet another compiler-compiler, (1979)
[28] Kajler, Norbert, Cas/pi: a portable and extensible interface for computer algebra systems, (Proceedings ISSAC ’92, (1992)), 376-386 · Zbl 0964.68587
[29] Kajler, Norbert, Environnement graphique distribué pour le calcul formel, (1993), Université de Nice-Sophia Antipolis, PhD thesis
[30] Kajler, Norbert; Soiffer, Neil, A survey of user interfaces for computer algebra systems, J. Symb. Comput., 25, 2, 127-159, (feb 1998)
[31] Knuth, D. E., The texbook, (1984), Addison-Wesley
[32] Kohlhase, M., Omdoc, (2000)
[33] Lamport, L., Latex, A document preparation system, (1994), Addison-Wesley · Zbl 0852.68115
[34] MacKichan Software, (1998), Scientific workplace
[35] Mamane, L.; Geuvers, H., A document-oriented coq plugin for texmacs, (Mathematical User-Interfaces Workshop 2006, St Anne’s Manor, Workingham, UK, (2006))
[36] Maplesoft, Maple user manual, (2005-2012), Maplesoft, a division of Waterloo Maple Inc. Toronto, Maple is a trademark of Waterloo Maple Inc.
[37] Maxima, The maxima computer algebra system, (1998), (free version)
[38] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/hol, (1993)
[39] Owre, S.; Shankar, N.; Rushby, J., Pvs specification and verification system, (1992)
[40] Padovani, Luca; Zacchiroli, Stefano, From notation to semantics: there and back again, (MKM, (2006)), 194-207 · Zbl 1188.68283
[41] Rekers, J., Parsing generation for interactive environments, (1992), University of Amsterdam, PhD thesis
[42] Sacerdoti Coen, Claudio, A user interface for a mathematical system that allows ambiguous formulae, (Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, UITP 2008, Electron. Notes Theor. Comput. Sci., vol. 226, (2009)), 67-87 · Zbl 1291.68368
[43] Smirnova, E.; Watt, S. M., Generating tex from mathematical content with respect to notational settings, (Proceedings of the International Conference on Digital Typography & Electronic Publishing: Localization & Internationalization, (2006)), 96-105
[44] Soiffer, Neil M., The design of a user interface for computer algebra systems, (1991), University of California at Berkeley, PhD thesis
[45] Soiffer, Neil, Mathematical typesetting in Mathematica, (Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, ISSAC ’95, (1995), ACM New York, NY, USA), 140-149 · Zbl 0922.68142
[46] Stamerjohanns, Heinrich; Ginev, Deyan; David, Catalin; Misev, Dimitar; Zamdzhiev, Vladimir; Kohlhase, Michael, Mathml-aware article conversion from latex, (Towards a Digital Mathematics Library, Grand Bend, Ontario, Canada, July 8-9th, 2009, (2009), Masaryk University Press), 109-120 · Zbl 1176.68233
[47] Stein, W. A., Sage mathematics software, (2004), The Sage Development Team
[48] Sussman, G. J.; Steele, G. L., Scheme, (1975)
[49] Tejero-Cantero, A., Interference and entanglement of two massive particles, (September 2005), Ludwig-Maximilians Universität München, Master’s thesis
[50] The OpenMath Society, Openmath, (2003)
[51] Théry, Laurent; Bertot, Yves; Kahn, Gilles, Real theorem provers deserve real user-interfaces, SIGSOFT Softw. Eng. Notes, 17, 5, 120-129, (1992)
[52] Unicode Consortium, Unicode, (1991)
[53] W3C, Mathml, (1999)
[54] Watt, S. M., Exploiting implicit mathematical semantics in conversion between tex and mathml, (2002)
[55] Wolfram, S., Mathematica: A system for doing mathematics by computer, (1991), Addison-Wesley, Mathematica is a trademark of Wolfram Research, Inc.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.