Abstract. The Mmt language has been developed as a scalable representation and interchange language for formal mathematical knowledge. It permits natural representations of the syntax and semantics of virtually all declarative languages while making Mmt-based MKM services easy to implement. It is foundationally unconstrained and can be instantiated with specific formal languages. The Mmt API implements the Mmt language along with multiple backends for persistent storage and frontends for machine and user access. Moreover, it implements a wide variety of Mmt-based knowledge management services. The API and all services are generic and can be applied to any language represented in Mmt. A plugin interface permits injecting syntactic and semantic idiosyncrasies of individual formal languages. The Mmt Language Content-oriented representation languages for mathematical knowledge are usually designed to focus on either of two goals: (i) the automation potential offered by mechanically verifiable representations, as pursued in semi-automated proof assistants like Isabelle and (ii) the universal applicability offered by a generic meta-language, as pursued in XML-based content markup languages like OMDoc. The Mmt language [11] (Module system for Mathematical Theories) was designed to realize both goals in one coherent system. It uses a minimal number of primitives with a precise semantics chosen to permit natural and adequate representations of many individual languages. A key feature is foundation-independence: Mmt systematically avoids a commitment to a particular type theory or logic. Instead, it represents every formal system as an Mmt theory: domain theories (like the theory Group), logics (like first-order logic FOL), and logical frameworks (like LF [4] ) are represented uniformly as Mmt theories. These theories are related by the meta-theory relation, e.g., LF is the meta-theory of FOL, which in turn is the meta-theory of Group. Mmt uses this relation to obtain the semantics of a theory from that of its metatheory; thus, an external semantics (called the foundation), e.g., a research article or an implementation, only has to be supplied for the topmost meta-theories. For example, a foundation for LF can be given in the form of a type system. Theories contain typed symbol declarations, which permit the uniform representation of constants, functions, and predicates as well as -via the CurryHoward correspondence -judgments, inference rules, axioms, and theorems. Theories are related via theory morphisms, which subsume translations, functors, and models. Finally, Mmt provides a module system for building large theories and morphisms via reuse and inheritance.
It also serves as a basis for the MMT (Module system for Mathematical Theories) framework REF .
The MMT API: A Generic MKM System
ArXiv
ArXiv
Computer Science Mathematics