The MMT Language and System


MMT goes out of its way to be be generic and reusable. It does not commit to a particular that is implemented, and it does not commit to a particular application that this implementation is used for.

Foundation independence is discussed in more detail in this paper.

Application Independence

MMT is an API and as such not committed to particular applications. The MMT system includes several MMT-based applications that yield, e.g., build tools for MMT archives, a jEdit-based text editor, or a web server for MMT content.

Logic Independence

MMT is logic-independent, i.e., it is not commited to a particular logic. Therefore, MMT users have to define their logic in MMT or import a logic defined by someone else. MMT beginners should check out the MMT archive urtheories. This archive defines several basic languages, in particular the logical framework LF. Other archives can be found at OAF