OMDoc

From MathWeb

Jump to: navigation, search

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

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.

Distribution

The OMDoc distribution contains

Work in progress:

Also note:

Related Projects

Projects based on OMDoc

Auto-generated list:


Mentioned in


References

Personal tools
MathWeb
Structures