Towards MKM in the Large: Modular Representation and Scalable Software Architecture
Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev

TL;DR
This paper addresses the challenge of scaling mathematical knowledge management to large, interconnected corpora by proposing modular representation languages and scalable software architectures, exemplified by the MMT framework and TNTBase system.
Contribution
It introduces the MMT framework for modular theory-graphs and TNTBase, a versioned storage system, to support scalable, incremental processing of large mathematical knowledge bases.
Findings
MMT enables modular, scalable theory management.
TNTBase provides versioned storage for large XML-based documents.
Integration of MMT with TNTBase creates an effective MKM database.
Abstract
MKM has been defined as the quest for technologies to manage mathematical knowledge. MKM "in the small" is well-studied, so the real problem is to scale up to large, highly interconnected corpora: "MKM in the large". We contend that advances in two areas are needed to reach this goal. We need representation languages that support incremental processing of all primitive MKM operations, and we need software architectures and implementations that implement these operations scalably on large knowledge bases. We present instances of both in this paper: the MMT framework for modular theory-graphs that integrates meta-logical foundations, which forms the base of the next OMDoc version; and TNTBase, a versioned storage system for XML-based document formats. TNTBase becomes an MMT database by instantiating it with special MKM operations for MMT.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Mathematics, Computing, and Information Processing · Semantic Web and Ontologies
