Skip to content
Snippets Groups Projects
Select Git revision
  • master default
  • zolekode-master-patch-26857
  • zolekode-master-patch-78201
  • zolekode-master-patch-54259
  • zolekode-master-patch-38209
5 results
Blame Permalink
oaf.md 2.10 KiB 
layout: project

title: "OAF: An Open Archive for Formalizations"
shorttitle: OAF
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.

active: true
start_date: '2014'
end_date: 'June 2018'
publink: auto

people: 
    - mkohlhase
    - frabe
    - dmueller
    - jbetzendahl
    - kamann
    - jsee
    - rmarcus
    - mrupprecht

logo: public/dfg_logo.svg
funding: DFG
program: Normalverfahren
grantid: KO 2428/13-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.

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 tackles 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 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.