OMDoc history

The start of the development of OMDoc as a content-based representation format for mathematical knowledge was triggered by an e-mail by Alan Bundy to Michael Kohlhase in 1998, where he lamented the fact that one of the great hindrances of knowledge-based reasoning is the fact that formalizing mathematical knowledge is very time-consuming and that it is very hard for young researchers to gain recognition for formalization work. This led to the idea of developing a global repository of formalized mathematics, which would eventually allow peer-reviewed publication of formalized mathematical knowledge, thus generating academic recognition for formalization work and eventually lead to the much enlarged corpus of formalized mathematics that is necessary for knowledge-based formal mathematical reasoning. Young researchers would contribute formalizations of mathematical knowledge in the form of mathematical documents that would be both formal and thus machine-readable, as well as human-readable, so that humans could find and understand them.

After about 18 Months of development, Version 1.0 of the OMDoc format was released on November 1. 2000 to give users a stable interface to base their documents and systems on. It was adopted by various projects in automated deduction, algebraic specification, and computer-supported education. The experience from these projects uncovered a multitude of small deficiencies and extension possibilities of the format, that have been subsequently discussed in the OMDoc community.

OMDoc 1.1 was released on December 29. 2001 as an attempt to roll the uncontroversial and non-disruptive part of the extensions and corrections into a consistent language format. The changes to version 1.0 were largely conservative, adding optional attributes or child elements. Nevertheless, some non-conservative changes were introduced, but only to less used parts of the format or in order to remedy design flaws and inconsistencies of version 1.0.

OMDoc 1.2 is the mature version in the OMDoc 1 series of specifications. It was released on July 17. 2006 and contains almost no large-scale changes to the document format, except that Content MathML is now allowed as a representation for mathematical objects. But many of the representational features have been fine-tuned and brought up to date with the maturing XML technology (e.g. xml:id attributes now follow the XML ID specification and the Dublin Core elements follow the official syntax. The main development is that the OMDoc specification, the DTD, and schema are split into a system of interdependent modules that support independent development of certain language aspects and simpler specification and deployment of sub-languages. OMDoc1.2 freezes the development so that version 2 can be started off on the modules.