Advertisement
Published in:
2019 | OriginalPaper | Chapter
MMTTeX: Connecting Content and Narration-Oriented Document Formats
Author : Florian Rabe
Published in: Intelligent Computer Mathematics
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
Narrative, presentation-oriented assistant systems for mathematics such as
on the one hand and formal, content-oriented ones such as proof assistants and computer algebra systems on the other hand have so far been developed and used largely independently. The former excel at communicating mathematical knowledge and the latter at certifying its correctness.
on the one hand and formal, content-oriented ones such as proof assistants and computer algebra systems on the other hand have so far been developed and used largely independently. The former excel at communicating mathematical knowledge and the latter at certifying its correctness.MMTTeX aims at combining the advantages of the two paradigms. Concretely, we use
for the narrative and Mmt for the content-oriented representation. Formal objects may be written in MMT and imported into
documents or written in the
document directly. In the latter case, Mmt parses and checks the formal content during
compilation and substitutes it with
presentation macros.
for the narrative and Mmt for the content-oriented representation. Formal objects may be written in MMT and imported into
documents or written in the
document directly. In the latter case, Mmt parses and checks the formal content during
compilation and substitutes it with
presentation macros.Besides checking the formal objects, this allows generating higher-quality
than could easily be produced by hand, e.g., by inserting hyperlinks and tooltips into formulas. Moreover, it allows reusing formalizations across narrative documents as well as between formal and narrative ones. As a case study, the present document was already written with MMTTeX.
than could easily be produced by hand, e.g., by inserting hyperlinks and tooltips into formulas. Moreover, it allows reusing formalizations across narrative documents as well as between formal and narrative ones. As a case study, the present document was already written with MMTTeX.
as a semantic markup format. Math. Comput. Sci.