From MathWeb

OMDoc is a markup language based on XML for mathematical knowledge representation with numerous applications: creation of customized modules for e-learning, data exchange between different theorem provers, web services, and more. It has been developed by Michael Kohlhase and others at Jacobs University Bremen.

Contents 1 Levels 2 OMDoc as an ontology language for mathematics 3 Distribution 4 Related Projects 4.1 Projects based on OMDoc 5 Mentioned in 6 References

Levels

OMDoc represents knowledge on three levels (cf. chapter 3.2 of the specification):

object

formulae, usually written in Content MathML or OpenMath

statement

symbols, definitions, examples, theorems, proofs, …

theory

theories and morphisms between them

OMDoc as an ontology language for mathematics

OMDoc, as it is, can be used to model statements and theories about mathematical concepts. Adhering to certain conventions, you can use it for directly representing knowledge about mathematical concepts, e.g. that one concept is subsumed by another one.

• Knowledge that is representable in OMDoc

Distribution

The OMDoc distribution contains

• the documentation
• example files
• XSLT stylesheets for transforming documents
• An OWL-DL implementation of the document ontology behind OMDoc

Work in progress:

• addressing and naming in OMDoc 2.0
• JOMDoc (Java OMDoc API)

Also note:

• OMDoc MIME type

Related Projects

Projects based on OMDoc

Auto-generated list:

• F-Logic in OMDoc
• Locutor
• Metamath to OMDoc Bridge
• OMBase
• OMDoc client
• STeX

Mentioned in

• OMDoc (Book)

References

• homepage
• Subversion URL (for developers)
• Trac URL (bug tracker)
• Specification
• Wikipedia article
• Mailing lists: project-omdoc@jacobs-university.de (homepage), project-omdoc-dev@jacobs-university.de (homepage)