Herbrand Sequente und die skolemisierungs-freie CERES Methode

Abstract

A branch of mathematical logic is proof theory, which considers proofs as formal objects and is concerned with the analysis of their properties. One of the main theorems in proof theory is the cut-elimination theorem. It was proved by Gerhard Gentzen and states that the so-called cut-rule can always be eliminated from a formal proof system in the style of the sequent calculus LK. In real mathematical proofs, cut-elimination can be regarded as a method for eliminating lemmas. One property of cut-free proofs is that they only use subformulas of the formulas that are already present in the statement which has to be proved, i.e. they have the subformula-property. Gentzen's cut-elimination method is regarded as reductive cut-elimination. This method does not analyse the whole proof, but performs local proof rewriting steps on small parts of the proof. Another approach to cut-elimination is the method CERES (cut-elimination by resolution). In this method all cuts are analysed simultaneously and hence the global structure of the proof is taken into account. Roughly speaking, CERES extracts an unsatisfiable set of clauses, that encodes the structure of a proof containing cuts. A resolution refutation of this set of clauses serves as a skeleton for a proof containing at most atomic cuts. CERES-omegawas developed as CERES-method for higher-order logic and works, in contrast to CERES, with Skolem-free end-sequents. For the cut-elimination a new sequent calculus, LKsk, is introduced which does not contain the cut-rule. In the course of this work the idea of Skolem-free proofs was transferred to first-order logic, to gain a CERES-method which works in the presence of strong quantifiers in the end-sequent. We concentrate on the extraction of Herbrand sequents instead of the construction of the ACNF, a proof with at most atomic cuts. In the original CERES-method Herbrand sequents were extracted from the ACNF. We show, that the ACNF is not needed for the extraction and that the Herbrand sequents can be extracted from the resolution refutation and the corresponding projections. Our method for the extraction of Herbrand sequents is exponentially faster than the original, Skolem-free method.

Ein Teilgebiet der mathematischen Logik ist die Beweistheorie, welche Beweise als formale Objekte betrachtet und deren Eigenschaften untersucht. Einer der wichtigsten Sätze der Beweistheorie ist der Satz der Schnittelimination. Dieser wurde von Gerhard Gentzen bewiesen und besagt, dass die sogenannte Schnittregel aus einem formalen Beweissystem (in der Art des Sequentialkalküls LK) immer enfernt werden kann. Die Schnittelimination kann in konkreten mathematischen Beweisen als eine Methode zum Entfernen von Hilfssätzen (Lemmata) angesehen werden. Eine Eigenschaft schnittfreier Beweise ist, dass sie nur Teilformeln der Formeln im zu beweisenden Satz enthalten, d.h. dass sie die Teilformel-Eigenschaft besitzen. Gentzen-s Methode zur Schnittelimination wird als reduktive Schnittelimination betrachtet. Hier betrachtet man nicht den gesamten Beweis, sondern führt lokale Beweistransformationen an einem Teil des gesamten Beweises durch. CERES (cut-elimination by resolution) stellt einen alternativen Ansatz dar. Hier werden alle Schnitte gleichzeitig analysiert und somit wird die globale Struktur des Beweises berücksichtigt. Grob gesagt wird eine widerlegbare Klauselmenge extrahiert, welche die Struktur eines Beweises mit Schnitten repräsentiert. Die Resolutionswiderlegung dieser Klauselmenge dient als Skelett für einen Beweis, der höchstens atomare Schnitte enthält. CERES! wurde als CERES-Methode für Logik höherer Ordnung entwickelt und arbeitet, im Gegensatz zu CERES, mit skolemfreien End-Sequenten. Für die Schnittelimination wird ein neuer Sequentialkalkül, LKsk, eingeführt, der keine Schnittregel enthält. Im Zuge dieser Arbeit wurde die Idee von skolemfreien Beweisen auf Logik erster Ordnung überführt, um eine CERES-Methode zu entwickeln, welche auch mit starken Quantoren im End-Sequent arbeiten kann. Wir konzentrieren uns auf die Extraktion von Herbrand Sequenten und nicht auf das Erzeugen der ACNF, welche ein Beweis mit höchstens atomaren Schnitten ist. Herbrand Sequente wurden in der ursprünglichen CERES-Methode aus der ACNF erzeugt. Wir zeigen, dass man für die Extraktion die ACNF nicht benötigt und dass man die Herbrand Sequente bereits aus der Resolutionswiderlegung und den zugehörigen Projektionen gewinnen kann. Unsere Methode zur Extraktion von Herbrand Sequenten ist exponentiell schneller als die ursprüngliche skolemfreie Methode.