Im Rahmen des Fermat Projektes des IMMD8 sind Teilprojekte zusammengeführt, die die Anwendung der Künstlichen Intelligenz auf die Mathematik erforschen. Projektziel ist es, ein Assistenzsystem für Mathematiker zu entwickeln, das aus Komponenten zum

• Beweisen mathematischer Aussagen (Beweissystem),
• Entdecken interessanter mathematischer Aussagen (Entdeckungssystem),
• Lehren mathematischer Inhalte (Tutorsystem),
• Lesen mathematischer Texte (Hypertextsystem),
• Schreiben mathematischer Texte (Authoringsystem) und
• Auffinden mathematischen Wissens (Datenbanksystem)

In nachfolgenden Abschnitt werden nun einige der am IMMD VIII ausgeschriebenen Studien-und Diplomarbeiten motiviert und beschrieben.

Eine Datenbank für mathematisches Wissen

Innerhalb des Fermat-Projektes nimmt die Datenbank für mathematisches Wissen einen zentralen Platz ein. Dem Mathematiker soll ein komfortables Werkzeug zum Auffinden mathematischen Wissens bereitgestellt werden.

Die Mizar-Forschungsgruppe hat sich zur Aufgabe gemacht, grundlegende Theorien aus allen Bereichen der Mathematik zu formalisieren. Alle mit dem Beweisüberprüfungssystem Mizar verifizierten Beweise werden im Journal of Formalized Mathematics publiziert. Die Formalisierung (mehr als 2000 Definitionen und 20000 bewiesene Theoreme) besteht im Wesentlichen aus einer großen ungeordneten Ansammlung von Dateien; als Suchwerkzeug steht das grep-Kommando zur Verfügung.

Im Rahmen einer Diplomarbeit konnte diese Dateiensammlung in eine objekt-orientierte Datenbank transferiert werden. Aufbauend auf der objekt-orientierten Repräsentation des gesamten vom Mizar-Team geleisteten Formalisierung sind am IMMD VIII die folgenden Studien- und Diplomarbeiten als Folgearbeiten zu vergeben:

• Das Arbeiten mit MIZAR erfordert eine gute Kenntnis der mathematischen Bibliothek. Häufiges Suchen nach geeigneten Theoremen und Definitionen zur Rechtfertigung von Beweisschritten nimmt viel Zeit in Anspruch. Zur Zeit hat man nur die Möglichkeit, einen einmal in einem HTML-Browser dargestellten Text zu lesen und darin enthaltene Links zu verfolgen. Ziel ist es nun, gute Such- und Navigationsmethoden zum Browsen durch mathematische Theorien und zum Ermitteln im aktueller Beweiskontext anwendbarer Theoreme und Definitionen zu entwickeln. In diesem Rahmen soll nun die Spezifikation und Implementierung einer geeigneten und komfortablen Anfragesprache geleistet werden. Queries der folgenden Art sollten möglich sein:
  • Gib mir die Definition der Komposition von Funktionen!
  • Gib mir alle Theoreme, die etwas über die Eigenschaften des Kompositionsoperators auf Funktionen aussagen!
  • Gib mir alle Attribute, die einer Funktion zugesprochen werden können!
  • Gib mir alle Operatoren, die ich auf Funktionen anwenden kann!

  Weiterhin soll eine Schnittstelle zwischen einem html-Browser (z.B. Netscape) und der um die Anfragesprache angereicherte Datenbank entwickelt werden.

• Implementierung von diversen Ausgabeformaten. Wir unterscheiden zwischen der internen und externen Repräsentation des in der Datenbank enthaltenen formalen mathematischen Wissens. Innerhalb einer Studienarbeit sollen nun verschiedene externe Repräsentationen implementiert werden. Angestrebte Formate sind:
  • html: Anfrageergebnisse sollen als Hypertext dargestellt werden können.
  • diverse Normalformen wie KIF, CNF, DNF und NNF, sodaß Anfrageergebnisse direkt an Beweissysteme wie otter, setheo und dialog weitergeleitet werden können.
• Im Journal of Formalized Mathematics werden die mit MIZAR bewiesenen Theoreme veröffentlicht. Dabei werden automatisch die in der formalen Sprache MIZAR's formulierten Theoreme nach LaTeX in eine lesbarere Form konvertiert. Diese Konvertierung schließt die Formulierung der Beweise nicht ein. In der Studien-/Diplomarbeit soll versucht werden,
  • die Konvertierung der in der Eingabesprache von MIZAR formulierten Theoreme nach LaTeX zu optimieren;
  • diesen Konvertierungsalgorithmus auf die in der Eingabesprache von MIZAR formulierten Beweise zu erweitern. Ziel ist es, Theorem und Beweis in eine für Mathematiker lesbarere Form zu bringen.
• Es gibt eine Unzahl von Theorembeweisern. Um ein Theorembeweiser zu evaluieren und mit anderen Systemem zu vergleichen wurde die TPTP ("Thousands Problems for Theorem Provers") - eine Bibliothek, die unzählige Problemstellungen für Theorembeweiser enthält - entwickelt. Mithilfe eines Konvertierungstools können Problemstellungen aus TPTP in den jeweiligen Eingabeformalismus des im Test stehenden Beweisers konvertiert werden. TPTP wird "manuell" gepflegt, d.h. neue Problemstellungen müssen von Hand generiert und in TPTP aufgenommen werden. Ein großer Teil der Problemstellungen ist dabei nicht mathematisch motiviert; sonst zielt darauf ab, bestimmte Beweiser an bestimmte technische Grenzen zu führen. Ziel der TPTP ist es nicht, Mathematik zu formalisieren, wie es etwa die Mizar-Gruppe verfolgt.

  Im Rahmen einer Arbeit ist nun die Spezifikation und Implementierung eines Systems zu leisten, welches in der Lage ist, aus der Mizar-Datenbank formalisierten Wissens automatisch Beweisprobleme zu generieren. Damit soll die weltweit genutzte Standard-Bibliothek TPTP [SSY94] abgelöst werden.

• Untersuchungen zur weiteren Strukturierung der Datenbank in Theoriengebilde; Aufbau einer Landkarte mathematischen Wissens; Aufstellen von Taxonomien von Definitionen und Theoremen (Graphischer Browser); Ermitteln statistischer Informationen (Anzahl von Referenzen auf ein Theorem, etc.)
• Implementierung einer Umgebung zur Beweisentwicklung: Implementierung einer Schnittstelle zwischen xemacs und der Datenbank: Darstellung des extended ascii character set; Automatisches Einfügen von Beweisskeleten; syntax and parentheses highlighting; Interprozess-Kommunikation zwischen xemacs und der in Allegro Common Lisp/AllegroStore implementierten Datenbank.

Automatische Beweisüberprüfung

Existierende Beweisüberprüfer sind nicht in der Lage, natürlich-sprachliche Eingaben -- z.B. Beweistexte, die einem Lehrbuch zur elementaren Zahlentheorie entnommen sind -- zu verarbeiten. Liegt der mathematische Text dem Beweisüberprüfer aber formal -- etwa als Abfolge von Regelanwendungen des Sequentzenkalküls für Prädikatenlogik 1. Stufe mit Gleichheit - vor, so ist seine Überprüfung trivial. Ein Korrektheitsüberprüfung beschränkt sich auf das schrittweise Nachvollziehen der korrekten Anwendung von Kalkülregeln.

Interessant wird es, wenn der Beweis nur bruchstückhaft formal vorliegt. Es ist nun Aufgabe des Beweisüberprüfers, die fehlenden formalen Beweisschritte selbst zu erbringen, um die Lücken -- aber nicht mehr -- zu füllen. Der Beweisüberprüfer tritt damit als Beweiser auf.

Noch interessanter ist die Frage, inwieweit ein Beweisüberprüfer in der Lage ist, informelle Beweise zu überprüfen. In mathematischen Texten -- seien es nun Lehrbücher zur elemenaren Zahlenheorie oder in Fachzeitschriften veröffentlichte Artikel aus der aktuellen Forschung -- ist der formale Anteil der Beweise gering. Formale Beweise, in dem Sinn, daß sie in einem formalen Kalkül geführt worden sind oder geführt werden könnten, lassen sich in mathematischen Texten nicht finden. Sie wären auch nicht lesbar und verständlich. Der Mathematiker bedient sich vielmehr einer Fachsprache, mit der er versucht, mathematische Inhalte -- nicht formal, aber präzise -- zu vermitteln. Er reichert mathematische Beweise durch Zusatzinformationen, wie verwendete Beweismethode und Beweisfäden, an. Er verzichtet aus Gründen der Lesbarkeit und Verständlichkeit auf die Darstellung trivialer Beweisschritte. Dies stellt an ein System für automatische Beweisüberprüfung besondere Herausforderungen ([Sim90]).

Im Rahmen des Teilprojektes Automatische Beweisüberprüfung sind folgende Arbeiten zu vergeben: Es sind mathematische Beweise zu analysieren und zu beschreiben! Die zu untersuchenden Theoreme und ihre Beweise sind aus der elementaren Zahlentheorie und stammen aus [HW71]. Zunächst ist eine Klassifizierung der Beweise in Beweistypen (direkter Beweis, indirekter Beweis, etc.) vorzunehmen. Hilfreich dabei ist die Lekture von Solow's How to read and do proofs ([Sol90]).

Alle in [HW71] vorkommenden Beweise sind danach zu identifizieren. Dazu gehört auch die Markierung von Beweisanfängen und -enden sowie die Identifizeriung von Sätzen, die mit dem eigentlichen Beweisverlauf nicht zu tun haben (historische Anmerkungen, Anmerkungen zum Schwierigkeitsgrad des Beweises und sonstige Meta-Aussagen). Dabei sind auch verschachtelte Beweise -- ein Beweis zerfällt in mehrere Unterbeweise unterschiedlicher Beweistypen -- zu betrachten. In der Beweisbeschreibung sollten logische Beziehungen zwischen Aussagen, evtl. Beweispläne sowie die Offenlegung von Beweislücken nicht fehlen. Im Text stets wiederkehrende Phrasen sind zu identifizieren und in Semantik-erhaltende Standardphrasen zu transformieren.

Ziel ist die Entwicklung einer Beweisbeschreibungssprache!

email: zinn@immd8.informatik.uni-erlangen.de
http://www.informatik.uni-erlangen.de/IMMD8/staff/Zinn/zinn.html

Eine elektronische Fassung dieses Dokuments finden Sie im WWW:

http://www8.informatik.uni-erlangen.de/IMMD8/Research/fermat.html