OAF: An Open Archive of 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.