Using the technology from #24. We had this for the OAF project. Here is the old main page.
Overview
This is the MathHub-based portal for the archives of DFG OAF
Project (Open Archive of Formalizations).
The OAF project is a research project that aims at establishing an open
archive for formal mathematics and researching the technologies,
(meta)-logical foundations, and applications of such a system and
resource.
This knowledge hub contains OMDoc/MMT versions of the libraries of
paradigmatic theorem provers, together with formalizations of their
interface logics and theory morphisms between them. This makes the
libraries available in a uniform meaning space and in joint format, so
that they can be accessed together.
This is intended as the basis for "global" knowledge management services
like search, browsing via alignments, or library refactoring.
To interactively browse the content check the "Explore" tab above. Read
more about the MathHub system [[here|main]].
Using the technology from #24. We had this for the OAF project. Here is the old main page.
Overview
This is the MathHub-based portal for the archives of DFG OAF Project (Open Archive of Formalizations).
The OAF project is a research project that aims at establishing an open archive for formal mathematics and researching the technologies, (meta)-logical foundations, and applications of such a system and resource.
This knowledge hub contains OMDoc/MMT versions of the libraries of paradigmatic theorem provers, together with formalizations of their interface logics and theory morphisms between them. This makes the libraries available in a uniform meaning space and in joint format, so that they can be accessed together.
This is intended as the basis for "global" knowledge management services like search, browsing via alignments, or library refactoring.
To interactively browse the content check the "Explore" tab above. Read more about the MathHub system [[here|main]].