Computerunterstützte Analyse von Beweisen

Forschungsprojekt P 14126Computerunterstützte analyse von BeweisenMatthias BAAZ06.03.2000 Symbolisches Rechnen hat in zahlreichen Wissenschaften und Ingenieursdisziplinen zu einer Revolutionierung der Arbeitsweisen geführt, die sich auch in der weiten Verbreitung von Systemen wie Mathematica und Maple manifestiert. Es fehlen dabei allerdings Algorithmen, die sich mit der Analyse von Beweisen oder allgemeiner: formalisierten Entscheidungen befassen. Der wachsende Bedarf an solchen Algorithmen ergibt sich aus folgenden Überlegungen: * Mathematisches Wissen ist eher eine Kenntnis von Beweisen als von Fakten. Das heißt, dass die Analyse von Beweisen im Sinne einer automatisierten Entwicklung von Beweisstilen notwendig ist, wenn automatische Beweiser jemals die Beweisstärke menschlicher Beweiser erreichen sollen. * Da das mathematische Wissen ständig anwächst, wird interaktives Arbeiten für Mathematiker mehr und mehr an Bedeutung gewinnen: Mathematiker entwickeln Beweispläne und Programmsysteme vervollständigen die Details. Dazu ist es aber notwendig, dass diese Beweispläne durch die Programmsysteme korrekt interpretiert werden, d.h. dass es möglich ist, sie formal zu analysieren. * Die Analyse von Beweisen kann selbst zu neuen mathematischen Einsichten führen. Dazu gehören u.a. die Berechnung von Schranken und die Entnahme von Algorithmen aus nichtkonstruktiven Beweisen von Existenzsätzen sowie die Verallgemeinerung von Beweisen, die es ermöglicht, Beweise unmittelbar auf verwandte Problemstellungen zu übertragen. Die Automatisierung dieser Überlegungen in Verbindung mit den erwähnten Programmsystemen ermöglicht es dem Benutzer, zusätzliche mathematische Informationen mit geringem Aufwand zu erhalten. * Weiters dringen mathematische Anwendungen durch die fortschreitende allgemeine Automatisierung in Bereiche wie Rechtsabläufe oder industrielle Produktionsweisen vor, bei denen Schnittstellen zwischen mathematischem System und tatsächlichem Anwender unumgänglich sind. Solche Schnittstellen beruhen aber auf der formalen Analyse der zugrundeliegenden Argumentationsformen. Das vorliegende Projekt befasst sich mit der Weiterentwicklung und Implementierung von beweis-theoretischen Algorithmen zur Beweisanalyse. Die Beweistheorie ist jenes auf David Hilbert zurückgehende Teilgebiet der mathematischen Logik, das sich mit der Behandlung grundlagentheoretischer Fragen mit Hilfe von Beweistransformationen befasst. Die dabei entstandenen Algorithmen wurden aber wegen des vorherrschenden grundlagentheoretischen Interesses nur in Einzelfällen auf konkrete Beweise angewandt und niemals bis zur Implementationsreife weiterentwickelt. Die wichtigsten intendierten Algorithmen des vorliegenden Projektes beziehen sich dabei auf Schnittelimination und e -Elimination, die es sozusagen ermöglichen, mit Hilfssätzen geführte indirekte Beweise in direkte Beweise umzuwandeln. Als theoretische Grundlage ist es notwendig, eine Beweistheorie der Skolemfunktionen zu entwickeln (Skolemfunktionen erlauben es, Quantorenzusammenhänge durch funktionale Zusammenhänge zu ersetzen). Weiters sollen während des Projektverlaufes erstellte Verfahren unmittelbar auf konkrete mathematische Beweise angewendet werden um tatsächliche Verwendbarkeit zu garantieren. Gedacht ist dabei an die Lösung des berühmten Kugelproblems von Euler durch Schütte und van der Wærden ("Wieviele Punkte im Abstand eins können auf einer Kugel mit Radius eins liegen?") sowie an Einzelfälle der (durch Andrew Wiles bewiesenen) Fermatschen Vermutung. Die geplanten Anwendungen der implementierten Algorithmen zur Beweisanalyse umfassen * die Berechnung von Schranken und die Ermittlung von Programmen aus nichtkonstruktiven Beweisen * das Ersetzen von implizit definierten Konzepten durch explizite Definitionen mit Hilfe des Definierbarkeitstheorems von Beth * die Berechnung von Beweisverallgemeinerungen * die Berechnung von Beweissegmenten als Module für weiterführende Beweise. Diese Verfahren stellen eine Grundlage für die automatisierte Entwicklung von Beweisstilen für automatische Beweiser dar.

Im Gebiet des Symbolischen Rechnens wurden bereits viele Verfahren entwickelt um Wissenschafter und Techniker bei ihrer Arbeit zu unterstuetzen. Die automatisierte Analyse von vorgegebenen Beweisen und Entscheidungen wurde dabei aber eher vernachlaessigt. in naher Zukunft wird es aber einen grossen Bedarf nach derartigen Verfahren geben, denn mathematische Beweise stellen die Grundlage mathematischen Arbeitswissens dar. Mathematische Modelle und Theorien werden meistens durch die Analyse von Beweisen gewonnen. Ohne automatisierte Analyse von Beweisen gibt es daher keinen wirklichen Fortschritt auf dem Gebiet des Automatischen Beweisens. Die ungeheuere Erweiterung mathematischen Wissens wird die Mathematiker in naher Zukunft zwingen, interaktiv zu arbeiten, d.h. der Computer, der die Beweisansaetze vervollstaendigen soll muss in der Lage sein, diese zu analysieren. Nicht zuletzt fuehrt die Analyse von Beweisen zu neuen mathematischen Ergebnissen, z.B. die Berechnung von Schranken oder die Verallgemeinerung der Beweise. In diesem Projekt wurden logische Methoden zur automatisierten Beweisanalyse untersucht . Die wichtigste Methode ist dabei die Schnittelimination, mit deren Hilfe hochgradig abstrakte Beweise in elementare umgeformt werden koennen. Das erlaubt z.B. Beweisen Programme zu entnehmen, Schranken zu berechnen und vieles mehr. Mit Hilfe der Implementation von CERES kann die Schnittelimination jetzt auf effektive Weise automatisch durchgefuehrt werden. Mehrere Beweise in der Literatur (u.a.ein topologischer Beweis der Existenz unendlich vieler Primzahlen) wurden mit den entwickelten Hilfsmitteln analysiert. (Im Fall des genannten Beweises stellte sich ueberaschenderweise heraus, dass er genau dem Euklidschen Beweis entspricht.)