Abstract
There is a large ecosystem of mathematical software systems. Individually, these are optimized for particular domains and functionalities, and together they cover many needs of practical and theoretical mathematics. However, each system specializes on one particular area, and it remains very difficult to solve problems that need to involve multiple systems. Some integrations exist, but the are ad-hoc and have scalability and maintainability issues. In particular, there is not yet an interoperability layer that combines the various systems into a virtual research environment (VRE) for mathematics.
The OpenDreamKit project aims at building a toolkit for such VREs. It suggests using a central system-agnostic formalization of mathematics (Math-in-the-Middle, MitM) as the needed interoperability layer. In this paper, we report on a case study that instantiates the MitM paradigm the systems GAP, SageMath, and Singular to perform computation in group and ring theory.
Our work involves massive practical efforts, including a novel formalization of computational group theory, improvements to the involved software systems, and a novel mediating system that sits at the center of a star-shaped integration layout between mathematical software systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Incidentally, this group is called \(D_4\) in SageMath but \(D_8\) in GAP due to differing conventions in different mathematical communities – a small example of the obstacles to system interoperability that MitM tackles.
- 2.
Of course, definitions are one possible way to specify the semantics of MitM-symbols.
- 3.
However, as we see below, this may still be surprisingly difficult in practice.
- 4.
In the future MMT might even serve as an external type-checker for GAP.
References
Cremona, J.: The L-functions and modular forms database project. Found. Comput. Math. 16(6), 1541–1553 (2016). https://doi.org/10.1007/s10208-016-9306-z
Dehaye, P.-O., et al.: Interoperability in the OpenDreamKit project: the Math-in-the-Middle approach. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 117–131. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_9. https://github.com/OpenDreamKit/OpenDreamKit/blob/master/WP6/CICM2016/published.pdf
Freundt, S., et al.: Symbolic computation software composability protocol (SCSCP). Version 1.3. https://github.com/OpenMath/scscp/blob/master/revisions/SCSCP_1_3.pdf. Accessed 27 Aug 2017
The GAP Group: GAP - groups, algorithms, and programming. http://www.gap-system.org. Accessed 30 Aug 2016
Project Jupyter. http://www.jupyter.org. Accessed 22 Aug 2017
Kohlhase, M., et al.: The planetary system: Web 3.0 & active documents for STEM. Procedia Comput. Sci. 4, 598–607 (2011). https://doi.org/10.1016/j.procs.2011.04.063. Sato, M., et al. (eds.) Special issue: Proceedings of the International Conference on Com- putational Science (ICCS). Finalist at the Executable Paper Grand Challenge
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. http://omdoc.org/pubs/omdoc1.2.pdf
The LMFDB Collaboration: The L-functions and modular forms database. http://www.lmfdb.org. Accessed 02 Jan 2016
MitM/Foundation. https://gl.mathhub.info/MitM/Foundation. Accessed 01 Sept 2017
MitM/Groups. https://gl.mathhub.info/MitM/groups. Accessed 01 Sept 2017
MMT - Language and System for the Uniform Representation of Knowledge. Project web site. https://uniformal.github.io/. Accessed 30 Aug 2016
Müller, D., et al.: Alignment-based translations across formal systems using interface theories. In: Fifth Workshop on Proof eXchange for Theorem Proving - PxTP 2017 (2017). http://jazzpirate.com/Math/AlignmentTranslation.pdf
Müller, D., Gauthier, T., Kaliszyk, C., Kohlhase, M., Rabe, F.: Classification of alignments between concepts of formal mathematical systems. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 83–98. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_7
OpenMath CD Group: polygrp. http://www.openmath.org/cdgroups/polygrp.html. Accessed 01 Sept 2017
An OpenMath 2.0 implementation in Python. https://github.com/OpenMath/py-openmath. Accessed 04 Sept 2016
An SCSCP module for Python. https://github.com/OpenMath/py-scscp. Accessed 04 Sept 2016
Rabe, F.: The MMT API: a generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 339–343. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_25
Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1–54 (2013). http://kwarc.info/frabe/Research/mmt.pdf
The Sage Developers: SageMath, the sage mathematics software system. http://www.sagemath.org. Accessed 30 Sept 2016
Singular. https://www.singular.uni-kl.de/. Accessed 22 Aug 2017
Acknowledgements
The authors gratefully acknowledge the fruitful discussions with other participants of work package WP6, in particular Alexander Konovalov on SCSCP, Paul Dehaye on the SageMath export and the organization of the MitM ontology, and Luca de Feo on OpenMath phrasebooks and the SCSCP library in python. We acknowledge financial support from the OpenDreamKit Horizon 2020 European Research Infrastructures project (#676541) and DFG project RA-18723-1 OAF.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Kohlhase, M. et al. (2017). Knowledge-Based Interoperability for Mathematical Software Systems. In: Blömer, J., Kotsireas, I., Kutsia, T., Simos, D. (eds) Mathematical Aspects of Computer and Information Sciences. MACIS 2017. Lecture Notes in Computer Science(), vol 10693. Springer, Cham. https://doi.org/10.1007/978-3-319-72453-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-72453-9_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72452-2
Online ISBN: 978-3-319-72453-9
eBook Packages: Computer ScienceComputer Science (R0)