Abstract
The paper presents the format for representing informal mathematics. acts as a surface language for two systems: the (presentation-oriented) system to produce PDF and the semantics-aware Mmt system for advanced knowledge management services. We discuss how the markup facilities allow in situ flexiformalization (and the necessary elaboration of complex structures), while staying presentationally neutral.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Note that the latter requires a browser with MathML support to display formal expressions, such as Firefox, but notably not (vanilla) Chrome yet (intent-to-publish for MathML in Chromium has been announced, expected in 2023).
- 2.
This case requires a symbol for conjunction to be in scope, which can be marked as such using a dedicated parametric Mmt rules. The expression above (and now here, too) type checks, because we include a module that provides one earlier.
References
Carette, J., Farmer, W.M., Kohlhase, M.: Realms: a structure for consolidating knowledge about mathematical theories. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 252–266. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_19
Müller, D., Rabe, F., Rothgang, C., Kohlhase, M.: Representing structural language features in formal meta-languages. In: Benzmüller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 206–221. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53518-6_13
Horozal, F., Rabe, F., Kohlhase, M.: Flexary operators for formalized mathematics. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 312–327. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_23
Kohlhase, M., Müller, D.: The sTeX3 package collection. Technical Report. https://github.com/slatex/sTeX/blob/main/doc/stex-doc.pdf. Accessed 24 Apr 2022
Kohlhase, M.: OMDoc – an open markup format for mathematical documents [version 1.2]. LNCS (LNAI), vol. 4180. Springer, Heidelberg (2006). https://doi.org/10.1007/11826095
Kohlhase, M.: Using LATEX as a semantic markup format. Math. Comput. Sci. 2(2), 279–304 (2008). https://doi.org/10.1007/s11786-008-0055-5, https://kwarc.info/kohlhase/papers/mcs08-stex.pdf
MMT – Language and System for the Uniform Representation of Knowledge. Project web site. https://uniformal.github.io/. Accessed 15 Jan 2019
Müller, D., Rabe, F., Kohlhase, M.: Theories as types. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 575–590. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_38
Müller, D.: Mathematical knowledge management across formal libraries. PhD thesis. Informatics, FAU Erlangen-Nürnberg, December 2019. https://opus4.kobv.de/opus4-au/files/12359/thesis.pdf
Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 0.230, 1–54 (2013). https://kwarc.info/frabe/Research/mmt.pdf
sTeX: a semantic extension of TeX/LaTeX. https://github.com/sLaTeX/sTeX. Accessed 05 Nov 2020
Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.): CICM 2014. LNCS (LNAI), vol. 8543. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Müller, D., Kohlhase, M. (2022). Injecting Formal Mathematics Into LaTeX. In: Buzzard, K., Kutsia, T. (eds) Intelligent Computer Mathematics. CICM 2022. Lecture Notes in Computer Science(), vol 13467. Springer, Cham. https://doi.org/10.1007/978-3-031-16681-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-031-16681-5_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-16680-8
Online ISBN: 978-3-031-16681-5
eBook Packages: Computer ScienceComputer Science (R0)