Mathematical Knowledge Management Across Formal Libraries

Language
en
Document Type
Doctoral Thesis
Issue Date
2019-11-11
Issue Year
2019
Authors
Müller, Dennis
Editor
Abstract

This dissertation is concerned with the problem of integrating formal libraries: There is a plurality of theorem prover systems and related software with different strengths and weaknesses, that are fundamentally incompatible. This is due to different input languages, IDEs, library management facilities etc., but also due to fundamental theoretical aspects; primarily the reliance on different logical foundations, such as set theories, type theories, and additional primitive features (e.g. subtyping, specific module systems,...).

This thesis describes the approach towards solving this problem pursued at our research group. Specifically, it is divided into three main parts:

  1. I demonstrate how we can develop modular logical frameworks within the MMT system – a foundation-agnostic framework for formal knowledge management based on the OMDoc/MMT language. This allows for specifying almost arbitrarily complicated logics, type theories and related systems. An important aspect of such a framework is the ability to include potentially complex and computationally expensive features (such as subtyping mechanisms or record types) on demand only.
  2. We can use this framework to formalize the logical foundation – or, if nonexistent, at least the foundational ontology – of a formal system, which we can use in turn to translate the associated libraries to OMDoc/MMT. I demonstrate this exemplary on the theorem prover PVS, the computer algebra systems Sage and GAP, and the LMFDB database.
  3. This enables accessing the core concepts and libraries of various systems from within the MMT system, and hence implement knowledge management services generically, acting on multiple libraries at once. I present a few such services: (a) Curating alignments (roughly: two symbols S, T are called aligned if they represent the same platonic mathematical concept), (b) a generic method for translating formal expressions between systems and libraries; using known alignments, theory morphisms and (if necessary) programmatic tactics, (c) an algorithm for automatically finding morphisms between theories (modulo alignments, if between theories from different libraries) and (d) Theory Intersections as a method to refactor given theories using theory morphisms.
Abstract

Diese Doktorarbeit widmet sich dem Integrationsproblem formaler Bibliotheken: Es gibt eine Vielzahl an Theorembeweisern und verwandter formaler Software mit unterschiedlichen Stärken und Schwächen, die grundlegend inkompatibel sind. Dies liegt sowohl an unterschiedlichen Eingabesprachen, IDEs, Bibliotheksmanagement etc., als auch grundlegenden theoretischen Aspekten; primär die Verwendung unterschiedlicher logischer Fundamente, wie Mengentheorien, Typentheorien, und zusätzlichen primitiven Features (z.B. Subtyping, spezifische Modulsysteme,...).

Die Arbeit beschreibt den von unserer Forschungsgruppe verfolgten Ansatz, dieses Problem anzugehen. Konkret ist sie in drei zentrale Abschnitte geteilt:

  1. Ich zeige, wie wir innerhalb des MMT Systems – einem fundament-agnostischen Framework für formales Wissensmanagement mit zugrundeliegender Sprache OMDoc/MMT – logische Frameworks modular entwickeln können, was es uns erlaubt nahezu beliebig komplexe Logiken, Typentheorien und ähnliche fundamentale Systeme darin zu spezifizieren. Wichtig ist hierbei, dass die potentiell komplexen Features die wir dafür auf Ebene des logischen Frameworks brauchen (wie Subtyping-Mechanismen oder record types) auch nur dort aktiv sind, wo wir sie explizit brauchen.
  2. Dieses Framework können wir nun nutzen um die logischen Fundamente – oder, falls nicht vorhanden, zumindest die zugrundeliegende Ontologie – eines formalen Systems zu formalisieren, und auf Basis dessen die zugehörigen Bibliotheken nach OMDoc/MMT zu übersetzen, was ich am Beispiel des Beweissystems PVS, den Computeralgebrasystemen Sage und GAP, und der LMFDB Datenbank demonstriere.
  3. Dies innerlaubt es uns, innerhalb des Mmt Systems auf die zugrundeliegenden Konzepte verschiedener Systeme und deren Bibliotheken zuzugreifen, und entsprechende Services zu implementieren die auf mehreren verschiedenen Bibliotheken agieren. Entsprechend stelle ich einige solcher Features vor: (a) Das kuratieren von Alignments (Grob: zwei symbole S, T heißen aligned, wenn sie das selbe abstrakte/platonische mathematische Konzept repräsentieren), (b) eine generische Methode, formale Ausdrücke zwischen Systemen und Bibliotheken zu übersetzen; unter Verwendung bekannter Alignments, Theoriemorphismen und (notfalls) programmatischen Methoden, (c) einen Algorithmus, der Morphismen zwischen Theorien findet (modulo Alignments, falls zwischen unterschiedlichen Bibliotheken) und (d) Theory Intersections als eine Methode, gefundene Theoriemorphismen auszunutzen um gegebene Theorien zu refaktorisieren.
DOI
Faculties & Collections
Zugehörige ORCIDs