OAF: An Open Archive of Formalizations

OAF：形式化的开放档案

• 批准号: 247572299
• 负责人: Professor Dr. Michael Kohlhase
• 金额: --
• 依托单位: Department Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2014
• 资助国家: 德国
• 起止时间: 2013-12-31 至 2019-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/247572299?language=en
• 关键词: OAF; Open; Archive; Formalizations

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.

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