Titelaufnahme

Titel
Herbrand sequent extraction / Bruno Woltzenlogel Paleo
VerfasserWoltzenlogel Paleo, Bruno
Begutachter / BegutachterinLeitsch, Alexander
Erschienen2007
UmfangXI, 78 S.
HochschulschriftWien, Techn. Univ., Mag.-Arb., 2007
Anmerkung
Zsfassung in dt. Sprache
SpracheEnglisch
Bibl. ReferenzOeBB
DokumenttypMasterarbeit
Schlagwörter (DE)Sequentkalkül / Logik
Schlagwörter (EN)First Order Logic / Sequent Calculus / Logic / Automated Deduction
URNurn:nbn:at:at-ubtuw:1-18086 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Herbrand sequent extraction [0.47 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Nach der Definition einer Verallgemeinerung des Herbrandschen Theorems für Sequente, beschreiben wir drei schon existierende Algorithmen für die Extraktion eines Herbrandsequents aus formalen Beweisen, die im Sequentialkalkül LK geschrieben sind. Darüber hinaus verbessern wir diese drei Algorithmen und entwicklen daraus einen vierten Algorithmus, welcher deren Ideen vereinigt und generalisiert.

Dieser Algorithmus wurde dann realisiert und in das CERes (Cut-Elimination by Resolution) Projekt integriert. Die Wichtigkeit der Extraktion von Herbrandsequenten liegt darin, dass Herbrandsequente die Kreativität der Beweise enthält.

Zusammenfassung (Englisch)

After defining a generalization of Herbrand's Theorem for sequents, we describe three pre-existing algorithms for the extraction of a Herbrand sequent of the end-sequent of proofs in the Sequent Calculus LK. Furthermore, we improve these three algorithms by designing a new fourth algorithm, which combines and generalizes their essential ideas. The implementation of this new algorithm was realized within the framework of the project CERes (Cut-Elimination by Resolution). The importance of extracting Herbrand sequents from proofs lies on the fact that a Herbrand sequent summarizes the creative content of a proof.