Abstrakte Beweisstrukturen : ein einheitliches Framework

Abstract

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.

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.