toolsprojects.md

layout	title
default	OMDoc Tools and Projects

A representation format is only as good as the respective tools and systems are. Therefore tool development will be the main concern in the next future.

General XML tools for OMDoc

• DTD and Schema-based Validation
• the TNTBase system, a versioned XML database witt OMDoc support, it can be used to store, query and reference mathematical documents represented in OMDoc.

OMDoc Libraries

• The main development platform is [jomdoc:WikiStart JOMDoc] (a Java-based OMDoc library).
• [mmt:WikiStart FLOMDoc] is an experimental library in SCALA.

Tools to support the management and creation of OMDocs

• the semantic wiki SWiM for editing, browsing, and discussing OMDoc
• the CPoint system, allows to annotate M$ PowerPoint slides and export OMDoc
• The ActiveMath Project has provided some authoring tools as well.
• The sTeX system is a semantic extension of TeX/LaTeX that supports translation into OMDoc.
• and a bunch of XSL style files to present OMDoc to the user (part of the above-mentioned JOMDoc) and transform it into input formats of various mathematical software systems.

Projects that that endorse OMDoc (see also the systems below)

• ActiveMath (Math Learning on the Web)
• Course Capsules (Content based course delivery at Carnegie Mellon)
• OMEGA (a mathematical assistant)

Systems that speak OMDoc (varying degrees of fluency)

• LambdaClam (an inductive theorem prover)
• INKA (another inductive theorem prover)
• TPS (a higher-order theorem prover)
• OMEGA (a mathematical assistant)
• VeriFun (a verifier for functional programs)

OMDoc Interfaces for Existing Systems

• an Interface to the PVS system.
• an Interface to the Coq theorem prover via the HELM XML interface.
• an Interface for the Aldor programming language (only developed for OMDoc 1.1).