Aus mathematischen Beweisen lässt sich explizite Information gewinnen, welche nicht im Theorem sichtbar ist. Um diese Art von Information aus Beweisen gewinnen zu können, arbeitet man mit Beweisen in Normalform, also analytischen Beweisen ohne Schnittregeln. In dieser Arbeit interessieren wir uns insbesondere für Herbrand Sequenzen. Herbrand Sequenzen sind propositional gültige Sequenzen, welche aus Instanzen des entsprechenden Theorems erstellt werden und realisieren dadurch den Satz von Herbrand im Sequenzenkalkül. Bisher wurden Herbrand Sequenzen aus Beweisen in Normalform mit einer effizienten Schnitteliminationsmethode, der Methode CERES, extrahiert. Wir zeigen, dass Beweise nicht unbedingt in Normalform sein müssen um Herbrand Sequenzen extrahieren zu können. Unsere Methode beruht auf speziellen Eigenschaften der CERES Methode für die Beweisanalyse. Da Herbrand Sequenzen nur aus Beweisen von pränexen Endsequenzen extrahiert werden können, verallgemeinern wir die Methode um Expansionsbeweise (eine Verallgemeinerung von Herbrand Sequenzen) zu gewinnen. Die entwickelten Methoden sind implementiert und an einigen Beispielbeweisen veranschaulicht. In einem letzten Schritt verallgemeinern wir unsere Methoden um auch mit Beweisen, welche Induktionsregeln beinhalten, arbeiten zu können. Wir wählen die Darstellung von Beweisen als Beweisschemata, welche die Erstellung von sogenannten Herbrand Systemen ermöglichen, und entwickeln eine schematische CERES Methode, welche mit komplizierteren Sätzen arbeiten kann als bestehende Methoden zur Beweisanalyse induktiver Beweise. Das Ziel dieser Forschung ist eine völlig automatisierte Analyse von interessanten mathematischen Beweisen, wie zum Beispiel von Fürstenbergs Beweis über die Unendlichkeit der Primzahlen. Obwohl eine völlig automatisierte Analyse dieses Beweises noch nicht erreicht werden konnte, stellt diese Arbeit einen wichtigen Schritt in der Entwicklung dar.
de
Mathematical proofs can be used to extract explicit information about mathematical objects that is not visible in the theorem itself. In general, this kind of information can be extracted only from proofs in normal form, i.e. analytic proofs without cuts. In this work we are particularly interested in the extraction of Herbrand sequents from proofs. Herbrand sequents are propositionally valid sequents composed of instances of a corresponding theorem, thus they are a realization of Herbrands theorem in sequent calculus. So far, Herbrand sequents are extracted from proofs in normal form using the method CERES, which is a method specifically designed for efficient cut-elimination. In this work we show that for Herbrand sequent extraction proofs need not be in normal form. This novel method is based on specific features of the CERES method and simplifies and outperforms the current CERES method for proof analysis. Moreover, as the usual method for Herbrand sequent extraction only works for proofs of prenex end-sequents, we generalize our novel method to the extraction of expansion proofs (a generalization of Herbrand sequents in a non-prenex setting). The developed methods are implemented and we demonstrate some experiments with mathematical proofs. In a last step we lift our methods to the case with induction rules. We represent induction via schemata of proofs, as proof schemata allow the extraction of so-called Herbrand systems. We define a schematic CERES method that is capable of handling several induction parameters and thus allows to analyze more complicated proofs outside the range of previously defined methods. The overall goal is to develop a fully automated analysis of interesting mathematical proofs, as for instance Fürstenbergs proof of the infinitude of primes. Though a fully automated analysis of this proof is not yet within reach, this work can be seen as a major step in the development.
en
Additional information:
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
