zbMATH — the first resource for mathematics

Supporting user-defined notations when integrating scientific text-editors with proof assistance systems. (English) Zbl 1202.68372
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, 176-190 (2007).
Summary: In order to foster the use of proof assistance systems, we integrated the proof assistance system \(\Omega\)mega with the standard scientific text-editor TEX\(_{\text{MACS}}\). We aim at a document-centric approach to formalizing and verifying mathematics and software. Assisted by the proof assistance system, the author writes her document entirely inside the text-editor in a language she is used to, that is a mixture of natural language and formulas in LaTeX style. We present a basic mechanism that allows the author to define her own notation inside a document in a natural way, and use it to parse the formulas written by the author as well as to render the formulas generated by the proof assistance system. To make this mechanism effectively usable in an interactive and dynamic authoring environment, we extend it to efficiently accommodate modifications of notations, to track dependencies to ensure the right order of notations and formulas, to use the hierarchical structure of theories to prevent ambiguities, and to reuse concepts together with their notation from other documents.
For the entire collection see [Zbl 1119.68011].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68U15 Computing methodologies for text processing; mathematical typography
Full Text: DOI