Bibliographic Metadata

Title
Proof transformations by resolution : computational methods of cut-elimination / Clemens Richter
AuthorRichter, Clemens
CensorLeitsch, Alexander ; Baaz, Matthias
Published2006
Description88 S.
Institutional NoteWien, Techn. Univ., Diss., 2006
Annotation
Zsfassung in dt. Sprache
Bibliographic Source
http://www.logic.at/people/richter/phdthesis.pdf
LanguageEnglish
Bibl. ReferenceOeBB
Document typeDissertation (PhD)
Keywords (DE)Beweistheorie / Schnittelimination / Beweistransformation / Beweisanalyse / Resolution / Paramodulation
Keywords (EN)proof theory / cut-elimination / proof transformation / proof analysis / resolution / paramodulation
Keywords (GND)Beweistheorie / Schnittelimination / Resolution <Logik>
URNurn:nbn:at:at-ubtuw:1-19752 Persistent Identifier (URN)
Restriction-Information
 The work is publicly available
Files
Proof transformations by resolution [0.57 mb]
Links
Reference
Classification
Abstract (German)

In der Beweistheorie werden Beweise als formale Objekte repräsentiert.

Schnittelimination ist eine auf Gentzen zurückzuführende Disziplin, welche eine bestimmte Regel - die Schnittregel - aus diesen formalen Beweisen entfernt.

Diese Technik der Beweistransformation hat sich zu einer der bedeutendsten Disziplinen der Beweistheorie entwickelt. Der Effekt der Schnittelimination ist die Entfernung aller Anwendungen von Hilfsaussagen (Lemmata) innerhalb eines Beweises, was wiederum zu einem analytischen Beweis, im Sinne dass alle Aussagen innerhalb des Beweises Teilformeln des sich ergebenden Satzes sind, führt.

Die Schnitteliminationsmethode CERES (Schnittelimination mittels Resolution) analysiert zunächst die konkrete Beweisstruktur und bildet diese auf eine unerfüllbare Klauselmenge ab. Eine Resolutionswiderlegung dieser Klauselmenge dient dann als Skelett für eine analytische Variante des Beweises.

Die Gleichheit ist ein zentrales Paradigma in der Mathematik und spielt eine Schlüsselrolle in der automatischen Deduktion. Diese Bedeutung weckt daher die Notwendigkeit die Gleichheit in bestehende Schnitteliminationskonzepte zu integrieren. In dieser Arbeit wird eine Erweiterung von CERES zu CERESe, durch das Hinzufügen der Gleichheit in Form von Regeln zu den zugrunde liegenden Sequentialkalkülen, präsentiert wobei alle Vorzüge von CERES erhalten bleiben. Insbesondere bleibt CERESe den Schnittreduktionsystemen ähnlich zu Gentzen's Ansatz überlegen, sie ist flexibel bezüglich Resolution in Verbindung mit Paramodulation und all deren Verfeinerungen und erlaubt eine semantische Verwendung des Schnitts. Wir erweitern CERES auch durch das Konzept der Gleichheitstheorien was neben den bereits bestehenden Vorteilen der Methode zu einem System führt, das in erster Linie eine Vereinfachung der Beweisnotation mit sich bringt.

Weiters wird eine Implementierung von CERES in Form eines Computersystems zur Schnittelimination vorgestellt, welches die Transformation von konkreten, mathematisch relevanten Beweisen erlaubt. Das System unterstützt die beweistheoretische Analyse von Beweisen und ist auch in der Lage schnittfreie Beweisvarianten zu erzeugen, die sich hinsichtlich ihrer Argumentation deutlich unterscheiden. Dies ist die erste Implementierung eines solchen Systems und könnte der Anfang einer neuen Ära von computergestützter Beweistheorie sein. Einige Experimente mit konkreten, aussagekräftigeren Beweisen, die bereits einen gewissen Komplexitätsgrad aufweisen runden die Demonstration des Systems ab.

Abstract (English)

In proof theory mathematical proofs are represented as formal objects.

Cut-elimination is a discipline due to Gentzen removing a certain rule - the cut rule - from these formal proofs. This proof transformation technique has advanced to one of the most important disciplines in proof theory. The effect of cut-elimination is the removal of all applications of intermediate statements (lemmas) within a proof resulting in a proof that is analytic in the sense, that all statements of the proof are subformulas of the resulting theorem.

The cut-elimination method CERES (cut-elimination by resolution) first analyzes and maps a proof structure to a clause term which evaluates to an unsatisfiable set of clauses. A resolution refutation of this clause set then serves as a skeleton for an analytic variant of the proof.

Equality is a central paradigm in mathematics and plays a key role in automated deduction. Therefore its importance awakes the necessity of integrating equality into existing cut-elimination concepts. In this thesis an extension of CERES to CERESe by adding equality in form of rules to the underlying sequent calculi is presented where all the benefits of CERES are preserved.

In particular CERESe is superior to Gentzen like cut-reduction systems, it is flexible with respect to resolution in conjunction with paramodulation and all its refinements and admits a semantical use of cut. We also enrich CERES by the concept of equational theories yielding a system which adds mainly simplicity of proof notations to the existing advantages of the method.

Furthermore an implementation of CERES as a computational system for cut-elimination is presented allowing the transformation of concrete mathematically relevant proofs. The system supports the proof theoretical analysis of proofs and is also capable of generating variants of cut-free proofs which are clearly distinguishable by their argumentation. This is the first implementation of such a system and could be the beginning of a new era of computational proof theory. Some experiments with concrete proofs of some relevance which already have a certain complexity round off the demonstration of the system.