Third party funded individual grant
Acronym: OAF
Start date : 01.01.2014
End date : 30.06.2020
Extension date: 30.06.2020
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.
Mathematisches Wissen liegt im Kernbereich von Wissenschaft und Technologie und ist ein wesentlicher Innovationsfaktor. Allerdings wächst das verfügbare Wissen schneller als unsere Fähigkeit es zu organisieren und zu nutzen. Maschinelle Unterstützung durch symbolische (Software)-Systeme könnte theoretisch Abhilfe schaffen, aber benötigt in der Regel Bibliotheken formalisierten mathematischen Hintergrundwissens. Somit wird die maschinelle Unterstützung durch die hohen Formalisierungskosten ausgebremst. Schlimmer noch: Die Systeme und ihre Bibliotheken sind nicht interoperabel, da sie auf unterschiedlichen logischen Grundlagen aufbauen. So gehen Ressourcen durch Parallelentwicklung grundständiger Bibliotheken verloren, die dann wiederum für die Abdeckung neuer Wissensgebiete fehlen. Zudem zwingt die Pluralität der Bibliotheksformate zur Parallelentwicklung von Bibliotheksmanagementfunktionalitäten statt die originären Systemfunktionalitäten zu verbessern.Das beantragte OAF-Projekt trägt zur Lösung der Interoperabilitäts- und Pluralitätsprobleme durch die Entwicklung eines offenen Archivs für Formalisierungen bei, also einer gemeinschaftlichen Infrastruktur zur Nutzung und zum Management formalen mathematischen Wissens wie Theorien, Definitionen, oder Beweisen. Diese Infrastruktur ist auf Skalierbarkeit sowohl über große Wissensmengen als auch über unterschiedliche logische Grundlagen ausgelegt. Insbesondere basiert es auf einem einheitlichen metalogischen Repräsentationsformat, in dem die logischen Grundlagen zusammen mit den Bibliotheken formalisiert werden, so dass es als Fundament für die semantische Vernetzung von Bibliotheken dienen kann.Dadurch wird das OAF Projekt zwei wichtige Engpässe beseitigen. Zum einen stellt es eine allgemeine Archivlösung bereit, die sich nicht alle einzelnen Arbeits- oder Nutzergruppen alleine leisten können. Zum anderen liefert es ein standardisiertes, systemübergreifendes Bibliotheksformat, das die Vergleichbarkeit und dadurch die Evolution von Systemen katalysiert.Entwickler symbolischer Systeme können das Bibliotheksmanagement an das OAF-System delegieren, und die Mathematical Knowledge Management (MKM) Community kann auf der Basis von OAF Mehrwertdienste entwickeln. Im Gegensatz zum momentanen Stand der Technik können sich die Entwickler symbolischer Systeme auf die logischen Grundlagen ihrer Systeme konzentrieren und die Entwickler generischer MKM-Dienste erhalten Zugang zu Bibliotheken relevanter Größe. Unsere systemübergreifende Repräsentationssprache ermöglicht -- zum ersten Mal -- die systematische Erforschung der Integration von großen Bibliotheken verschiedener Formalismen. Längerfristig ermöglicht dies die nahtlose Verknüpfung und Verschmelzung von Bibliotheken zu einem großen formalen Wissensraum.