Previous: TR 95-10 Next: TR 95-12


Intellektik: Technical report 95-11

Repräsentation von Konnektionsbeweisen in Gentzen-Kalkülen durch Transformation und Strukturierung

Karin Genther

Die vorliegende Diplomarbeit befaßt sich in einem ersten Teil mit der Transformation von Extensionsbeweisen in den natürlichen Kalkül NK von Gentzen. Zu Beginn werden die erforderlichen logischen und deduktiven Grundlagen zur Verfügung gestellt. Anschließend werden die für die Transformation benötigten Begriffe eingeführt und die Transformationsregeln und der Algorithmus zur Transformation vorgestellt. Im zweiten Teil der Arbeit werden verschiedene Möglichkeiten zur Strukturierung natürlicher Beweise untersucht. Das Hauptaugenmerk liegt dabei auf der Strukturierung von Beweisen durch Einführung von Schnittformeln und der Darstellung der Beweise im Sequenzenkalkül LK (mit Schnittregel) von Gentzen. Zur Erzeugung der Schnittformeln werden exemplarisch die Methoden der Reduktion, Antipränexierung und die Funktionseinführung benutzt.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry