Automatische Analyse mathematischer Beweise

Seit der Zeit der Griechen sind Beweise das wissenschaftliche Fundament der Mathematik. Sie dienen dabei nicht nur der Verifikation, sondern sind zugleich Indikator und Quelle für Algorithmen und mathematische Methoden. In diesem Kontext spielt die Beweisanalyse und die Beweistransformation eine wichtige Rolle: So ermöglicht die Transformation in elementare Beweise (durch die Schnittelimination) die Extraktion von Herbrand Sequenten, Schranken und Algorithmen (und damit schliesslich auch von Programmen). Ein Programm für die automatische Schnittelimination (im Gentzenkalkül LK) wurde im Rahmen des FWF Projektes P 16264 auf Basis der CERES (cut-elimination by resolution) Methode entwickelt. Dieses Programm ist in der Lage Schnitte in großen und komplexen LK Beweisen zu eliminieren, weil es auf der Resolutionsmethode beruht, die den eigentlichen Kern der Methode darstellt. Das Anliegen dieses Projektes lässt sich in zwei Punkten beschreiben: 1. die Erweiterung der CERES Methode für "echte" mathematische Beweise. Dafür soll eine eigene Sprache für Beweise (auf der Basis von Einführung und Elimination von Definitionen) und ein Programm zur einfachen Eingabe von großen und komplexen Beweisen entwickelt werden. Der eigentliche Kern der CERES Methode soll um Algorithmen zur Behandlung der Gleichheit und zur effizienten Extraktion von Herbrand Sequenten erweitert werden. 2. soll die theoretische Analyse der CERES Methode vertieft werden, im speziellen für Logik höherer Stufe und für die intutionistische Logik. Damit könnte der Grundstein für eine effiziente Schnittelimination in der Mathematik höherer Ordnung gelegt werden. Die theoretische und praktische Arbeit an der Methode hat das Ziel ein System für die voll- und halbautomatische Beweistransformation zu entwickeln. Dieses sollte vor allem Mathematikern bei der Analyse und Entwicklung von mathematischen Beweisen dienen.

Seit der Zeit der Griechen sind Beweise das wissenschaftliche Fundament der Mathematik. Sie dienen dabei nicht nur der Verifikation, sondern sind zugleich Indikator und Quelle für Algorithmen und mathematische Methoden. In diesem Kontext spielt die Beweisanalyse und die Beweistransformation eine wichtige Rolle: So ermöglicht die Transformation in elementare Beweise (durch die Schnittelimination) die Extraktion von Herbrand Sequenten, Schranken und Algorithmen (und damit schliesslich auch von Programmen). Ein Programm für die automatische Schnittelimination (im Gentzenkalkül LK) wurde im Rahmen des FWF Projektes P 16264 auf Basis der CERES (cut-elimination by resolution) Methode entwickelt. Dieses Programm ist in der Lage Schnitte in großen und komplexen LK Beweisen zu eliminieren, weil es auf der Resolutionsmethode beruht, die den eigentlichen Kern der Methode darstellt. Das Anliegen dieses Projektes lässt sich in zwei Punkten beschreiben: 1. die Erweiterung der CERES Methode für "echte" mathematische Beweise. Dafür soll eine eigene Sprache für Beweise (auf der Basis von Einführung und Elimination von Definitionen) und ein Programm zur einfachen Eingabe von großen und komplexen Beweisen entwickelt werden. Der eigentliche Kern der CERES Methode soll um Algorithmen zur Behandlung der Gleichheit und zur effizienten Extraktion von Herbrand Sequenten erweitert werden. 2. soll die theoretische Analyse der CERES Methode vertieft werden, im speziellen für Logik höherer Stufe und für die intutionistische Logik. Damit könnte der Grundstein für eine effiziente Schnittelimination in der Mathematik höherer Ordnung gelegt werden. Die theoretische und praktische Arbeit an der Methode hat das Ziel ein System für die voll- und halbautomatische Beweistransformation zu entwickeln. Dieses sollte vor allem Mathematikern bei der Analyse und Entwicklung von mathematischen Beweisen dienen.