Towards Semantic Markup of Mathematical Documents via User Interaction

Mathematical documents written in often contain ambiguities. We can resolve some of them via semantic markup using, e.g., , which also has other potential benefits, such as interoperability with computer algebra systems, proof systems, and increased accessibility. However, semantic markup is more involved than “regular” typesetting and presents a challenge for authors of mathematical documents. We aim to smooth out the transition from plain to semantic markup by developing semi-automatic tools for authors. In this paper we present an approach to semantic markup of formulas by (semi-)automatically generating grammars from existing macro definitions and parsing mathematical formulas with them. We also present a GUI-based tool for the disambiguation of parse results and showcase its functionality and potential using a grammar for parsing untyped \(\lambda \) -terms.