The OMDoc Format

OMDoc (Open Mathematical Documents; see the OMDoc book for details) was developed by Michael Kohlhase.

It can be seen as two things:

  • a philosophy of how a uniform language for knowledge should be designed
  • an XML format following this philosophy.

MMT fully subscribes to the OMDoc philosophy and can thus be seen as a concrete incarnation of OMDoc. Currently, MMT covers and heavily redesigns the formal subset of OMDoc (though work on the informal subset is currently under way).

Moreover, MMT has become a major driver of changes to the XML format or its specification.