DC FieldValueLanguage
dc.contributor.advisorLeitsch, Alexander-
dc.contributor.authorRietdijk, Mariëlle-
dc.date.accessioned2020-06-29T20:31:55Z-
dc.date.issued2018-
dc.date.submitted2019-04-
dc.identifier.citation<div class="csl-bib-body"> <div class="csl-entry">Rietdijk, M. (2018). <i>Extracting programs from proofs : using Friedman’s A-translation and realizability</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-124515</div> </div>-
dc.identifier.urihttps://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-124515-
dc.identifier.urihttp://hdl.handle.net/20.500.12708/8452-
dc.descriptionZusammenfassung in deutscher Sprache-
dc.description.abstractDas Thema dieser Dissertation basiert auf der starken Verbindung zwischen mathematischen Beweisen und Programmen, in dem Sinne, dass Beweise einen Rechengehalt haben, zusätzlich zur bloßen Vermittlung der Wahrheit ihrer Schlussfolgerung. Insbesondere beschreiben wir eine Methode zum Extrahieren von Programmen aus gegebenen klassischen arithmetischen Beweisen erster Ordnung von $\Pi_2$-Sätzen. Dies geschieht mit Hilfe einer Beweisübersetzung, die klassische Beweise in intuitionistische Beweise umwandelt, und einer Realisierbarkeitsinterpretation, die es erlaubt, intuitionistische Zeugen für Sätze aus ihren Beweisen in Form von Programmen zu extrahieren. Wir werden Kolmogorovs negative Übersetzung und Friedman's A-Übersetzung verwenden, um die Beweise zu transformieren und Realisatoren nach Kreisels modifizierter Realisierbarkeit zu extrahieren. Wir interessieren uns speziell für diese intuitionistischen Zeugen für Theoreme, weil sie Programme in Bezug auf eine Spezifikation sind, die in der Schlussfolgerung des Beweises ausgedrückt wird. Eine logische Formel $A$ mit den freien Variablen $x_1,\dots,x_r$ und $y$ kann als Spezifikation verstanden werden, wobei ein Programm, das diese Spezifikation erfüllt, eine Funktion $f$ berechnet, so dass für alle möglichen Eingabewerte $n_1,\dots,n_r$, der Satz $A[n_1 / x_1] \dots [n_r / x_r] [f (n_1, \dots, n_r) / y]$ wahr ist. Die in dieser Arbeit beschriebene Methode extrahiert Programme, die solchen Spezifikationen $A$ entsprechen, aus Beweisen, die die Existenz einer Funktion für $A$ implizieren, also aus Beweisen von Sätzen $\forall x_1 \dots \forall x_r \exists y A$. Insbesondere bietet uns die Realisierbarkeitsinterpretation eine Möglichkeit, Programme aus konstruktiven Beweisen zu extrahieren, und die Beweistransformation ermöglicht uns, diese Extraktion auch auf klassische Beweise auszuweiten.de
dc.description.abstractDas Thema dieser Dissertation basiert auf der starken Verbindung zwischen mathematischen Beweisen und Programmen, in dem Sinne, dass Beweise einen Rechengehalt haben, zusätzlich zur bloßen Vermittlung der Wahrheit ihrer Schlussfolgerung. Insbesondere beschreiben wir eine Methode zum Extrahieren von Programmen aus gegebenen klassischen arithmetischen Beweisen erster Ordnung von $\Pi_2$-Sätzen. Dies geschieht mit Hilfe einer Beweisübersetzung, die klassische Beweise in intuitionistische Beweise umwandelt, und einer Realisierbarkeitsinterpretation, die es erlaubt, intuitionistische Zeugen für Sätze aus ihren Beweisen in Form von Programmen zu extrahieren. Wir werden Kolmogorovs negative Übersetzung und Friedman's A-Übersetzung verwenden, um die Beweise zu transformieren und Realisatoren nach Kreisels modifizierter Realisierbarkeit zu extrahieren. Wir interessieren uns speziell für diese intuitionistischen Zeugen für Theoreme, weil sie Programme in Bezug auf eine Spezifikation sind, die in der Schlussfolgerung des Beweises ausgedrückt wird. Eine logische Formel $A$ mit den freien Variablen $x_1,\dots,x_r$ und $y$ kann als Spezifikation verstanden werden, wobei ein Programm, das diese Spezifikation erfüllt, eine Funktion $f$ berechnet, so dass für alle möglichen Eingabewerte $n_1,\dots,n_r$, der Satz $A[n_1 / x_1] \dots [n_r / x_r] [f (n_1, \dots, n_r) / y]$ wahr ist. Die in dieser Arbeit beschriebene Methode extrahiert Programme, die solchen Spezifikationen $A$ entsprechen, aus Beweisen, die die Existenz einer Funktion für $A$ implizieren, also aus Beweisen von Sätzen $\forall x_1 \dots \forall x_r \exists y A$. Insbesondere bietet uns die Realisierbarkeitsinterpretation eine Möglichkeit, Programme aus konstruktiven Beweisen zu extrahieren, und die Beweistransformation ermöglicht uns, dieseen
dc.formatxiii, 60 Seiten-
dc.languageEnglish-
dc.language.isoen-
dc.subjectBeweistheoriede
dc.subjectProgrammextraktionde
dc.subjectProof Theoryen
dc.subjectprogram extractionen
dc.titleExtracting programs from proofs : using Friedman's A-translation and realizabilityen
dc.typeThesisen
dc.typeHochschulschriftde
dc.publisher.placeWien-
tuw.thesisinformationTechnische Universität Wien-
tuw.publication.orgunitE192 - Institut für Logic and Computation-
dc.type.qualificationlevelDiploma-
dc.identifier.libraryidAC15353167-
dc.description.numberOfPages60-
dc.identifier.urnurn:nbn:at:at-ubtuw:1-124515-
dc.thesistypeDiplomarbeitde
dc.thesistypeDiploma Thesisen
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openaccessfulltextOpen Access-
item.openairetypeThesis-
item.openairetypeHochschulschrift-
item.fulltextwith Fulltext-
item.languageiso639-1en-
item.grantfulltextopen-
item.cerifentitytypePublications-
item.cerifentitytypePublications-
Appears in Collections:Thesis

Files in this item:


Page view(s)

14
checked on Aug 18, 2021

Download(s)

24
checked on Aug 18, 2021

Google ScholarTM

Check


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