Die Methode der Schnittelimination nimmt als Kern von Gerhard Gentzens Hauptsatz eine wichtige Rolle im Bereich der Logik ein.<br />Verwendet ein Beweis jedoch das Induktionsprinzip, ist Schnittelimination im Allgemeinen nicht mehr möglich. Ein Ansatz ist, Schnittelimination für eine abzählbar unendliche Folge von Beweisen, ein sogenanntes Beweisschema, zu definieren. Da das Resultat nun ebenfalls ein Beweisschema ist, lassen sich die auf reduktiven Ansätzen basierenden Methoden nicht mehr anwenden. Das dabei auftretende Problem ist, dass eine Schnittregel nicht immer schrittweise in Richtung der Axiome verschoben werden kann. Daher muss auf eine andere Schnitteliminationstechnik zurückgegriffen werden.<br />Die Schnitteliminationsmethode CERES basiert auf dem Konzept der charakteristischen Klauselmenge. Diese wird aus einem Beweis im Sequenzkalkül extrahiert und ist immer unerfüllbar. Eine Resolutionswiderlegung dieser Klauselmenge wird als Vorlage für einen neuen Beweis herangezogen, der nur mehr Schnitte über Atomformeln enthält. Dazu wird jede Klausel durch eine Projektion des ursprünglichen Beweises ersetzt und jeder Resolutionsschritt als Schnitt über einer Atomformel nachvollzogen. Damit analysiert CERES im Gegensatz zu den reduktiven Methoden alle Schnittformeln auf einmal.<br />Diese Dissertation verallgemeinert CERES sowohl für Aussagenlogik als auch für Prädikatenlogik erster Stufe auf Beweisschemata. Dazu wird der Sequenzkalkül LKS eingeführt, der die Darstellung von Beweisschemata mittels primitiver Rekursion zulässt. Es wird gezeigt, wie sich Schemata für die charakteristische Klauselmenge und die Beweisprojektionen erstellen lassen. Analog wird auch ein schematischer Resolutionskalkül definiert, der die Widerlegung der charakteristischen Klauselmenge erlaubt. Diese Widerlegung wird nun zusammen mit den Projektionen als Vorlage zur Konstruktion eines Beweisschemas herangezogen, das ausschließlich atomare Schnitte verwendet. Daraus ergibt sich eine Methode zur Schnittelimination für Beweisschemata.<br />
de
Gentzen's cut-elimination theorem is one of the most important theorems of logic. But it is proved that, in the presence of induction, cut-elimination is not possible in general. One way to overcome this problem is to define an infinite sequence of proofs in a uniform way (i.e. a proof schema), and do cut-elimination for the proof schema. This makes sense if the cut-free proofs also can be described uniformly. But the reductive methods fail to do so. The reason is that shifting cuts is not always possible in such proof schemata. Therefore another cut-elimination procedure is needed.<br />The cut-elimination method CERES (for first- and higher-order classical logic) is based on the notion of a characteristic clause set, which is extracted from an LK-proof and is always unsatisfiable. A resolution refutation of this clause set can be used as a skeleton for a proof with atomic cuts only (atomic cut normal form). This is achieved by replacing the input clauses from the resolution refutation by corresponding projections of the original proof. So, in contrast to reductive methods, CERES analyzes the proof as a whole.<br />We present a generalization of the CERES method to propositional and first-order proof schemata. We define a schematic version of the sequent calculus called LKS, and a notion of proof schema based on primitive recursive definitions. A method is developed to extract schematic characteristic clause sets and schematic projections from these proof schemata. We also define a schematic resolution calculus for refutation of schemata of clause sets, which can be applied to refute the schematic characteristic clause sets. Finally the projection schemata and resolution schemata are plugged together and a schematic representation of the atomic cut normal forms is obtained. Hence, we obtain a cut-elimination procedure for proof schemata.
