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.

Semantization

Knowledge Representation & Management

  • JOBAD

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

  • MathWebSearch

    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/MMT API

    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.

  • OAF: Open Archive of Formalizations

    The OAF Project builds a theoretical framework for interoperability of theorem prover libraries and implements an information system that host and align multiple libraries in a joint semantic setting.

  • OMDoc

    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.

  • Planetary

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

  • Semantic Alliance

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

Foundations of Math (on the web)

  • MMT/MMT API

    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.

  • OAF: Open Archive of Formalizations

    The OAF Project builds a theoretical framework for interoperability of theorem prover libraries and implements an information system that host and align multiple libraries in a joint semantic setting.