sTeX: Semantically Enhanced TeX

The last few years have seen the emergence of various content-oriented XML-based, content-oriented markup languages for mathematics on the web, e.g. OpenMath, Content MathML, or our own OMDoc. These representation languages for mathematics, that makes the structure of the mathematical knowledge in a document explicit enough that machines can operate on it. Other examples of content-oriented formats for mathematics include the various logic-based languages found in automated reasoning tools, program specification languages. The promise if these content-oriented approaches is that various tasks involved in ``doing mathematics'' (e.g. search, navigation, cross-referencing, quality control, user-adaptive presentation, proving, simulation) can be machine-supported, and thus the working mathematician is relieved to do what humans can still do infinitely better than machines: The creative part of mathematics --- inventing interesting mathematical objects, conjecturing about their properties and coming up with creative ideas for proving these conjectures. However, before these promises can be delivered upon (there is even a conference series studying ``Mathematical Knowledge Management (MKM)''), large bodies of mathematical knowledge have to be converted into content form.

Currently, a large part of mathematical knowledge is prepared in the form of TeX/LaTeX documents. Even though LaTeX goes a great step into the direction of an MKM format, it is not, as it lacks infrastructure for marking up the functional structure of formulae and mathematical statements, and their dependence on and contribution to the mathematical context.

In the sTeX project we investigate how we can use the macro language of TeX to make it into an MKM format by supplying specialized macro packages, which will enable the author to add semantic information to the document in a way that does not change the visual appearance. We speak of semantic pre-loading for this process and call our collection of macro packages (Semantic TeX). Thus, sTeX can serve as a conceptual interface between the document author and MKM systems: Technically, the semantically pre-loaded LaTeX documents are transformed into the (usually XML-based) MKM representation formats, but conceptually, the ability to semantically annotate the source document is sufficient.