Abstract
To support mathematical research, engineering, and education by computer systems, we need to deal with the differences between mathematical content collections and information systems available today. Unfortunately, these systems – ranging from Wikipedia to theorem prover libraries are usually only accessible via a dedicated web information system or a low-level API at the level of the raw database content. What we would want is a “programmatic, mathematical API” which would give access to the knowledge-bases programmatically via their mathematical constructions and properties.
This paper takes a step into this direction by interpreting large knowledge bases as OMDoc/MMT theories – modular representations of mathematical objects and their properties. For this, we generalize OMDoc/MMT theories to “virtual theories” – theories so big that they do not fit into main memory – and update its knowledge management algorithms so that they can work directly with objects stored in external knowledge bases. An additional technical contribution is the introduction of a codec system that bridges between low-level encodings in databases and the abstract construction of mathematical objects.
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
Similar content being viewed by others
Notes
- 1.
Technically, LMFDB is implemented using MongoDB and comprises a set of sets (each one called a database) of JSON objects. However, due to the conventions used, we can also understand it conceptually as a set of tables of a relational database, keeping in mind that every row is a tuple of arbitrary JSON objects.
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 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
Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_192
Kohlhase, M., et al.: Knowledge-based interoperability for mathematical software systems. In: Blömer, J., Kutsia, T., Simos, D. (eds.) MACIS 2017. LNCS, vol. 10693, pp. 195–210. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72453-9_14. https://github.com/OpenDreamKit/OpenDreamKit/blob/master/WP6/MACIS17-interop/crc.pdf
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
Luzhnica, E., Kohlhase, M.: Formula semantification and automated relation finding in the On-line Encyclopedia for integer sequences. In: Greuel, G.-M., Koch, T., Paule, P., Sommese, A. (eds.) ICMS 2016. LNCS, vol. 9725, pp. 467–475. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42432-3_60
LMFDB - API. http://www.lmfdb.org/api/. Accessed 17 Sept 2017
The LMFDB Collaboration: The L-functions and modular forms database. http://www.lmfdb.org. Accessed 01 Feb 2016
MathHub.info: Active mathematics. http://mathhub.info. Accessed 28 Jan 2014
MMT - Language and System for the Uniform Representation of Knowledge. Project web site. https://uniformal.github.io/. Accessed 30 Aug 2016
OpenDreamKit Open Digital Research Environment Toolkit for the Advancement of Mathematics. http://opendreamkit.org. Accessed 21 May 2015
OEIS Foundation Inc. (ed.): The On-line Encyclopedia of Integer Sequences. http://oeis.org. Accessed 28 May 2017
Rabe, F.: A query language for formal mathematical libraries. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 143–158. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_10. arXiv:1204.4685 [cs.LO]
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
Sloane, N.J.A.: The On-line Encyclopedia of integer sequences. Not. AMS 50(8), 912 (2003)
Wiesing, T.: Enabling cross-system communication using virtual theories and QMT. Master’s thesis, Jacobs University Bremen, Bremen, Germany, August 2017. https://github.com/tkw1536/MasterThesis/raw/master/thesis.pdf
Wikipedia: Wolfram language – Wikipedia, the free Encyclopedia (2017). https://en.wikipedia.org/w/index.php?title=Wolfram_Language. Accessed 09 Oct 2017
Wolfram-Alpha. http://www.wolframalpha.com. Accessed 05 Jan 2013
The LMFDB Collaboration: The L-functions and modular forms database. http://www.lmfdb.org. Accessed 27 Aug 2016
Acknowledgements
The authors gratefully acknowledge the fruitful discussions with other participants of work package WP6, in particular John Cremona on the LMFDB and Dennis Müller on early versions of the OMDoc/MMT-based integration. We acknowledge financial support from the OpenDreamKit Horizon 2020 European Research Infrastructures project (#676541).
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
Wiesing, T., Kohlhase, M., Rabe, F. (2017). Virtual Theories – A Uniform Interface to Mathematical Knowledge Bases. 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_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-72453-9_17
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)