A Module system for Mathematical Theories

This is the homepage of the MMT system designed and maintained by  Florian Rabe.

MMT is a language for formal mathematics that pays special attention to foundation-independence, scalability, and modularity. MMT is also a sublanguage of the  OMDoc format for open mathematical documents and will be integrated into the upcoming OMDoc 2 format.

The goals of OMDoc and MMT are to provide a web-scalable environment in which all mathematics can be represented in a way that supports both rigorous mathematical and logical tools as well as knowledge management services (e.g., databases, notation management, document management, change management).

I don't like fancy home pages with logos and animations. So don't let this site make you underestimate the system. Also while I usually keep this main page in sync with my research progress, other parts of the trac might be outdated.

MMT Language

The key features of the MMT language are

  • a module system for declarative languages that combines expressivity with simplicity,
  • a foundation- and logic-independent semantics,
  • a design that incorporates web-scalability.

The central concepts of the MMT syntax are

  • module level declarations
    • (structured) theories encapsulate mathematical contexts.
    • theory morphisms translate between theories either by representation (views) or by inheritance (structures),
    • styles are sets of notations to render MMT expressions for humans or systems.
  • symbol level declarations
    • constants represent mathematical objects as possibly typed, possibly defined entities akin to Pure Type Systems.
    • Axiom and theorem declarations are treated as special cases of symbols via the Curry-Howard correspondence.
    • notations state transformation rules in styles.
  • object level expressions
    • MMT integrates the OpenMath syntax for expressions but extends it with notions of theories and contexts.
    • morphisms are compositions of inclusions, views, and structures and are treated like objects in MMT.

MMT System

The MMT system consists of a  Scala-based reference API to the MMT data structures with a scriptable shell frontend and an HTTP

  • mmt-web, a  Lift-based HTTP server for mmt-api

The MMT svn repository can be accessed  here. It contains in particular, the mmt-api project and various plugins. These are eclipse projects, and they contain ant build files. Runnable jar files are provided in the  deploy directory.

Documentation

Quick installation instructions are given here.

Related Projects and Applications

MMT is heavily used in the  LATIN project. In particular, an instance of the LATIN web browser can be found  here.

In particular, LATIN uses MMT notations to produce  JOBAD-enabled XHTML-MathML.

MMT and JOBAD were used in our submission to the  AI Mashup Challenge.

Information on the MMT-Plugin for  TNTBase can be found  here.

MMT was used as the basis in the  Twelf module system. See here for more information.

Papers