KWARC: Current Projects

The KWARC group has developed various added value services based on OMDoc-encoded content, including a mathematical knowledge base, a semantic search engine, management of change, a semantic wiki, mathematical web services, and invasive OMDoc editing technologies. Furthermore, the group works on the utilization of OMDoc to provide Logic Interoperability and to establish scientific Communities of Practice.

Storage/Access

  • MMT is a framework for representing declarative languages such as logics, type theories, set theories, etc.. The MMT API implements complex algorithms generically for any language in the framework.

Representation

  • MMT is a framework for representing declarative languages such as logics, type theories, set theories, etc.. The MMT API implements complex algorithms generically for any language in the framework.

  • OMDoc is a markup format and data model for Open Mathematical Documents. It serves as semantics-oriented representation format and ontology language for mathematical knowledge.

  • Semantic Markup for LaTeX

Processing

  • Translating the arXiv.org to XML+MathML

  • The LaMaPUn project investigates the structure and meaning of scientific/technical documents and builds tools for extracting semantic representations from them that can be used to enhance access to and interaction with document corpora.

  • MMT is a framework for representing declarative languages such as logics, type theories, set theories, etc.. The MMT API implements complex algorithms generically for any language in the framework.

Interaction

  • JOBAD (JavaScript API for OMDoc-based Active Documents) is a javascript framework which makes it easy to create interactive web pages.

  • The MathWebSearch system (MWS) is a content-based search engine for mathematical formulae. It indexes MathML formulae, using a technique derived from automated theorem proving: Substitution Tree Indexing.

  • MMT is a framework for representing declarative languages such as logics, type theories, set theories, etc.. The MMT API implements complex algorithms generically for any language in the framework.

  • A framework for creating math-enabled Web 3.0 information portals.

  • The Semantic Alliance is a framework for mashing up semantic services into desktop applications.