Injecting formal mathematics into LaTeX

DOI10.1007/978-3-031-16681-5_12MaRDI QIDQ6160559zbMATH OpenOpenAlexFDO

Authors Dennis Müller, Michael Kohlhase

Publication date 2 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-16681-5_12

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Recommendations

• System description STEX3 -- a \LaTeX-based ecosystem for semantic/active mathematical documents
• Using La\TeX\ as a semantic markup format
• MMTTeX: connecting content and narration-oriented document formats
• Semantic preserving bijective mappings of mathematical formulae between document preparation systems and computer algebra systems
• Towards semantic mathematical editing

Cites work

• A scalable module system
• Flexary operators for formalized mathematics
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Realms: a structure for consolidating knowledge about mathematical theories
• Representing structural language features in formal meta-languages
• Theories as types
• Using La\TeX\ as a semantic markup format

Cited in

(6)

• Meta-stylesheets for the conversion of mathematical documents into multiple forms
• Growing the Digital Repository of Mathematical Formulae with Generic LaTex Sources
• Correctness of Copy in Calculi with Letrec
• Learning support systems based on mathematical knowledge management
• System description STEX3 -- a \LaTeX-based ecosystem for semantic/active mathematical documents
• Reusing learning objects via theory morphisms

This page was built for publication: Injecting formal mathematics into LaTeX

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160559)