Newer
Older
teaser: 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.
people:
- mkohlhase
- frabe
- dmueller
OAF was a DFG-funded research project running from 2014-2020 and headed by Michael Kohlhase
and Florian Rabe originally at Jacobs University Bremen and later at FAU Erlangen-Nürnberg.
It centered on the integration of formal mathematical libraries.
Both the [original proposal](http://kwarc.info/kohlhase/projects/oaf.pdf) and the [final report](../oaf-report.pdf) are available.
Formal/symbolic systems and their libraries are non-interoperable because they are based
on differing, mutually incompatible foundations (e.g., set theory, higher-order logic,
constructive type theory, etc.), library formats, and library structures, and much work is
spent developing basic libraries for mathematics in each system. Moreover, the ensuing
plurality of library formats forces implementors to spend time developing library
organization features (e.g., distribution, browsing, search, change management) for each
library format. All these investments bind resources that could be used to improve the
core functionality of the systems and the scope of the libraries.
The OAF project tackled these interoperability and plurality problems by developing an
open archive for formalizations, a common and open infrastructure for managing and sharing
formalized mathematical knowledge such as theories, definitions, and proofs. The OAF
infrastructure is designed to be scalable with respect to both the size of the knowledge
base and the diversity of logical foundations. In particular, the OAF system is based
on a uniform foundation-independent representation format for libraries, which allows
formalizing the logical foundations alongside the libraries and thus acts as framework for
aligning libraries.