Title: Extracting programs from proofs : using Friedman's A-translation and realizability
Language: English
Authors: Rietdijk, Mariëlle 
Qualification level: Diploma
Advisor: Leitsch, Alexander 
Issue Date: 2018
Citation: 
Rietdijk, M. (2018). Extracting programs from proofs : using Friedman’s A-translation and realizability [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-124515
Number of Pages: 60
Qualification level: Diploma
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.

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
Keywords: Beweistheorie; Programmextraktion
Proof Theory; program extraction
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-124515
http://hdl.handle.net/20.500.12708/8452
Library ID: AC15353167
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:


Page view(s)

10
checked on Jul 27, 2021

Download(s)

21
checked on Jul 27, 2021

Google ScholarTM

Check


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