From 88213344f4501c7ab6e75eb5e5e3b5ecf0811969 Mon Sep 17 00:00:00 2001 From: Florian Rabe <florian.rabe@gmail.com> Date: Wed, 20 Jan 2021 15:41:37 +0100 Subject: [PATCH] adding report --- projects/oaf.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/projects/oaf.md b/projects/oaf.md index 19c5961..b7eddca 100644 --- a/projects/oaf.md +++ b/projects/oaf.md @@ -27,9 +27,11 @@ grantid: KO 2428/13-1, RA 18723/1-1 proposal: http://kwarc.info/kohlhase/projects/oaf.pdf --- -OAF is a DFG-funded research project running from 2014-2017 and headed by Michael Kohlhase -and Florian Rabe at FAU Erlangen-Nürnberg. It aims at the integration of formal -mathematical libraries. +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](projects/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, @@ -40,11 +42,11 @@ organization features (e.g., distribution, browsing, search, change management) 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 tackles these interoperability and plurality problems by developing an +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 will be based +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. -- GitLab