<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://doi.org/10.34726/hss.2018.52485</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2018.52485
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/8452
-
dc.description
Zusammenfassung in deutscher Sprache
-
dc.description.abstract
Das 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.abstract
Das 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
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Beweistheorie
de
dc.subject
Programmextraktion
de
dc.subject
Proof Theory
en
dc.subject
program extraction
en
dc.title
Extracting programs from proofs : using Friedman's A-translation and realizability