Title: Herbrand sequent extraction
Language: English
Authors: Woltzenlogel Paleo, Bruno
Qualification level: Diploma
Keywords: Sequentkalkül; Logik
First Order Logic; Sequent Calculus; Logic; Automated Deduction
Advisor: Leitsch, Alexander
Issue Date: 2007
Number of Pages: 78
Qualification level: Diploma
Abstract: 
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.

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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-18086
http://hdl.handle.net/20.500.12708/14640
Library ID: AC05034889
Organisation: E185 - Institut für Computersprachen 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

File Description SizeFormat
Herbrand sequent extraction.pdf481.41 kBAdobe PDFThumbnail
 View/Open
Show full item record

Page view(s)

15
checked on Feb 18, 2021

Download(s)

87
checked on Feb 18, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.