OAF: Ein Offenes Archiv für Formalisierungen

• Antragsteller: Professor Dr. Michael Kohlhase; Privatdozent Dr. Florian Rabe
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 247572299

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.

• DFG-Verfahren: Sachbeihilfen