Overview

MMT is a framework for knowledge representation using formal languages such as logics, type theories, ontologies, set theories, etc.. It achieves a high level of generality by systematically avoiding a commitment to a representational paradigm, a particular concrete or abstract syntax, or a particular semantics.

Instead, individual features of the abstract syntax (e.g., lambda-abstraction, conjunction), the concrete syntax (e.g. keywords, notations), or the semantics (e.g., excluded middle, set theoretical interpretation) are defined as separate, reusable modules, from which individual languages are assembled.

Despite this high degree of abstraction, it is possible to implement advanced algorithms generically at the MMT level. The MMT system includes powerful generic solutions for knowledge management (e.g, IDE, change management) and verification (e.g., type reconstruction, module system).

By designing knowledge representation languages inside MMT, we can obtain strong implementations at extremely low cost.

A more detailed overview can be found in this paper.

What does MMT stand for?

The abbreviation means meta-meta-theory or meta-meta-tool, depending on whether you want to emphasize the theoretical or the practical aspects.

Here meta refers to using formal systems in which we represent, reason about, and implement languages. meta-meta means that we abstract even from the concrete formal system used to do that. This double meta level is a unique characteristic of MMT and, maybe surprisingly, makes it easier to build generic solutions than a single meta-level.

Structure of this Documentation

This is the main entry point to the MMT documentation. The documentation contains:

• practical instructions for getting started as a user as well tutorials for typical tasks
• a theoretical overview of the general philosophy behind MMT and the concrete language
• information about the structure of the MMT API
• documentation for individual applications built on top of the MMT API
• structure of the development of MMT

Acknowledgements

	MMT was partially supported by the DFG project OAF (grant agreements KO 2428/13-1 and RA 18723/1-1).
	MMT was partially supported by the Horizon 2020 European Research Infrastructure project OpenDreamKit (grant agreement #676541).

Disclaimer

MMT has been developed since 2005 and its theoretical foundation and practical implementation has become very mature. But it continues to be developed in parallel with the research that informs its design. Therefore, this documentation is occasionally incomplete or outdated.

We are committed to maintaining robust work flows for releasing, documenting, and bug-tracking to support large-scale applications. But that takes effort, and we prioritize according to the concrete research projects we are involved in.

If you have any questions or feedback – for example, if you want your particular use case to be better documented – don’t hesitate to contact me directly.