The OAF is a repository backend for mathematical content hosted at gl.mathhub.info
.
It is the main place to develop and publish MMT archives.
In particular, the OAF contains the following MMT archives:
archive | contents | depends on |
---|---|---|
MMT/urtheories | various top level languages, in particular the logical framework LF | |
MMT/examples | an example archive for beginners | MMT/urtheories |
MMT/experimental | similar to MMT/examples but not always working | MMT/urtheories |
MMT/LATIN | the LATIN logic atlas | MMT/urtheories |
MMT/LFX | (experimental) various LF extensions and modifications, e.g. subtyping, record types and HOTT | MMT/urtheories |
Mizar/mml | the Mizar Mathematical Library | MMT/LATIN |
TPTP/Distribution | the TPTP problem library | MMT/LATIN |
HOLLight/basic | the standard library of HOL Light | MMT/LATIN |
These archives can be installed and managed using lmh functionality provided by MMT.