OAF: An Open Archive of Formalizations

数学知识是科学和工程的核心，也是科学和工程的主要因素。 发达社会的创新。它的数量目前增长速度比我们的 组织和利用它的能力。通过符号（软件）系统的机器支持 将大大提高数学知识的潜力，但前提是 形式化背景知识库的存在。因此，机器支持是 受到形式化成本的阻碍。更糟糕的是，符号系统及其 库是不可互操作的，因为它们基于不同的基础， 许多工作都花在重新开发基础库上， 投资覆盖新领域。此外，随之而来的多种文库格式 迫使实施者花时间在图书馆组织特征上，而不是完善 系统的核心功能。 拟议的OAF项目解决了这些互操作性和多元化问题， 开发一个开放的正式档案，一个共同的和开放的基础设施， 管理和共享形式化的数学知识，如理论，定义， 和证据 OAF基础设施的设计是可扩展的， 知识库的规模和逻辑基础的多样性。 特别是 OAF系统将基于统一的基础独立表示格式， 库，它允许将逻辑基础与库一起形式化， 这将解决当前技术水平的两个主要瓶颈。它将提供一个永久的存档解决方案，不是所有系统和用户社区都能负担得起单独维护的费用。 它将建立一个标准化和开放的库格式，作为比较和系统进化的催化剂。符号系统开发人员将能够通过将他们的库导出到OAF中来委托库管理，数学知识管理（MKM）系统的开发人员将能够在其之上开发高级服务。这允许分离关注点：符号系统的开发人员可以专注于其系统的逻辑核心，而通用MKM服务的开发人员可以访问相关大小的库。最后，我们的档案馆的图书馆统一表示语言第一次使对以不同形式编写的大型库的集成进行了系统的大规模调查。 从长远来看，这使得图书馆能够无缝地组合和合并成一个通用的大规模知识空间。

Mathematical knowledge is at the core of science and engineering and a major factor in innovation in developed societies. Its quantity is currently growing faster than our ability to organize and utilize it. Machine support via symbolic (software) systems would greatly enhance the potential of mathematical knowledge, but is predicated on the existence of libraries of formalized background knowledge. Thus, machine support is hampered by the costliness of formalization. Even worse, symbolic systems and their libraries are non-interoperable because they are based on differing foundations, and much work is spent on re-development of basic libraries that could be more productively invested in covering new areas. Moreover, the ensuing plurality of library formats forces implementors to spend time on library organization features instead of perfecting the core functionality of their systems. The proposed 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 library and thus acts as framework for aligning libraries.This will resolve two major bottlenecks in the current state of the art. It will provide a permanent archiving solution that not all systems and user communities can afford to maintain separately. And it will establish a standardized and open library format that serves as a catalyst for comparison and thus evolution of systems.Symbolic system developers will be able to delegate library management by exporting their libraries into the OAF and developers of mathematical knowledge management (MKM) systems will be able to develop high-level services on top of it. Contrary to the current state of the art, this permits separating the concerns: developers of symbolic systems could focus on the logical core of their system and developers of generic MKM services gain access to relevant-size libraries.Finally, our archive's uniform representation language for libraries enables -- for the first time -- systematic large scale investigations into the integration of large libraries written in different formalisms. In the long run, this enables the seamless combining and merging of libraries into a universal large-scale knowledge space.