Titelaufnahme

Titel
Abstrakte Beweisstrukturen / von Andreas Humenberger
Weitere Titel
Abstract Proof Structures
VerfasserHumenberger, Andreas
Begutachter / BegutachterinHetzl, Stefan
ErschienenWien, 2016
Umfang63 Seiten
HochschulschriftTechnische Universität Wien, Univ., Diplomarbeit, 2016
Anmerkung
Arbeit an der Bibliothek noch nicht eingelangt - Daten nicht geprueft
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
SpracheEnglisch
DokumenttypDiplomarbeit
Schlagwörter (DE)Beweistheorie / Sequentialkalkül / Abstraktion / Framework / Äquivalenzrelation
Schlagwörter (EN)proof theory / sequent calculus / abstraction / framework / equivalence relation
URNurn:nbn:at:at-ubtuw:1-7070 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Abstrakte Beweisstrukturen [0.6 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Abstraktionen von formalen Beweisen, sogenannte abstrakte Beweisstrukturen, dienen als anerkanntes Werkzeug um Struktur und Eigenschaften von formalen Beweisen zu untersuchen. Für einen Beweis in einem Sequentialkalkül existieren verschiedenste Abstraktionen, wie Beweisskelett, Beweisnetz und Logischer Flussgraph (im speziellen Atomarer Flussgraph). Diese abstrakten Beweisstrukturen haben ihren Ursprung in verschiedenen Gebieten der Beweistheorie und eine gründliche Untersuchung der Zusammenhänge dieser existiert noch nicht. Durch die Definition einer Tupel-Darstellung von LK-Beweisen wird die Grundlage eines einheitlichen Rahmens zur Untersuchung von Beweisstrukturen im Sequentialkalkül LK gelegt. Diese Tupel-Darstellung erlaubt es, die oben genannten abstrakten Beweisstrukturen geeignet darzustellen und zu untersuchen. Wir zeigen, dass es bei geeigneter Behandlung der Abschwächung für jedes Paar der oben genannten Abstraktionen eine Struktur gibt, sodass beide zu dieser reduziert werden können. Neben den Einblicken in die Zusammenhänge der Beweisstrukturen entsteht ein Rahmen zur Verallgemeinerung von Resultaten und Algorithmen. So definierten etwa Krajicek und Pudlak einen Algorithmus zur Herleitung von Schranken bezüglich der minimalen Größe von Beweisen. Durch Verallgemeinerung dieses Algorithmus ergeben sich dieselben Schranken für Beweisnetze. Außerdem untersuchen wir die Kardinalitäten der Äquivalenzklassen, welche von den Abstraktionen generiert werden. Wir zeigen, dass es endlich viele Beweise gibt, welche dasselbe Beweisnetz (denselben Atomaren Flussgraphen) besitzen. Für Beweisskelette gibt es im Allgemeinen unendlich viele dazugehörige Beweise.

Zusammenfassung (Englisch)

Abstractions of formal proofs, so-called abstract proof structures, serve as a well-accepted tool for studying structure and properties of formal proofs. Given a sequent calculus proof, there are various abstractions including proof skeleton, proof net and logical flow graph (in particular atomic flow graph). These abstract proof structures emerged in different areas of proof theory and a thorough investigation of their interrelationship does not exist so far. By introducing a tuple-based representation of proofs, which allows a suitable representation of the before-mentioned abstractions, we establish a uniform framework for classical first-order logic which clarifies the relationship between these proof structures in the context of the sequent calculus LK. We show that, in case of a suitable treatment of the weakening rules, there exists a structure for every pair of the above-mentioned abstractions such that both abstractions can be reduced to it. Besides the gained insights of the interrelationship by defining this uniform framework, we get a framework for generalizing results and algorithms. For instance, Krajicek and Pudlak introduced an algorithm defined on proof skeletons for deriving bounds on the minimal size of proofs. We generalize this result to proof nets by generalizing the algorithm to proof net skeletons. A proof net skeleton is an abstraction of both, proof nets and proof skeletons. Furthermore, we investigate the cardinalities of the equivalences generated by the abstractions. We show that there exist finitely many proofs having the same proof net (atomic flow graph). For proof skeletons there exists an infinite number of associated proofs.