DC FieldValueLanguage
dc.contributor.advisorLeitsch, Alexander-
dc.contributor.authorWoltzenlogel Paleo, Bruno-
dc.date.accessioned2020-06-30T22:42:18Z-
dc.date.issued2007-
dc.date.submitted2007-06-
dc.identifier.urihttps://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-18086-
dc.identifier.urihttp://hdl.handle.net/20.500.12708/14640-
dc.descriptionZsfassung in dt. Sprache-
dc.description.abstractNach 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.<br />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.<br />de
dc.description.abstractAfter 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.en
dc.formatXI, 78 S.-
dc.languageEnglish-
dc.language.isoen-
dc.subjectSequentkalkülde
dc.subjectLogikde
dc.subjectFirst Order Logicen
dc.subjectSequent Calculusen
dc.subjectLogicen
dc.subjectAutomated Deductionen
dc.titleHerbrand sequent extractionen
dc.typeThesisen
dc.typeHochschulschriftde
tuw.publication.orgunitE185 - Institut für Computersprachen-
dc.type.qualificationlevelDiploma-
dc.identifier.libraryidAC05034889-
dc.description.numberOfPages78-
dc.identifier.urnurn:nbn:at:at-ubtuw:1-18086-
dc.thesistypeMasterarbeitde
dc.thesistypeMaster Thesisen
item.grantfulltextopen-
item.cerifentitytypePublications-
item.cerifentitytypePublications-
item.openairetypeThesis-
item.openairetypeHochschulschrift-
item.languageiso639-1en-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.fulltextwith Fulltext-
Appears in Collections:Thesis

Files in this item:

Show simple item record

Page view(s)

11
checked on Apr 19, 2021

Download(s)

91
checked on Apr 19, 2021

Google ScholarTM

Check


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