Organisator:

Priv.-Doz. Dr. Peter Schuster Mathematisches Institut Universität München Theresienstr. 39 80333 München, Germany

The objective is to present the developments that are taking place in the fields of proof mining, exhibiting the constructive content of classical proofs, formalisation of proofs, program extraction from proofs, and the like. The stress is on the proof-theoretic methods that have been used to improve on mathematical results by, for instance, enriching them systematically with algorithms and effective bounds. Examples are the formal approach to commutative algebra performed by Coquand and Lombardi, the monotone functional interpretation used by Kohlenbach in functional analysis, and the refined A-translation applied by Berger, Buchholz, and Schwichtenberg.

Auszug zu diesem Minisymposium aus dem Programmheft (Stand: 15. Juli 2006). Weitere nützliche Informationen rund um die Tagung können der verkürzten Ausgabe des Programmheftes entnommen werden.

Programm (Stand: 07.09.2006):

Donnerstag	Zeichensaal, Mathematisches Institut, Wegelerstr. 10
15:00-15:50	Henri Lombardi (Besançon, France) The Elimination of Prime Ideals
16:00-16:50	Ulrich Kohlenbach (Darmstadt) Logical Metatheorems and their Use in Functional Analysis and Hyperbolic Geometry
17:00-17:50	Bas Spitters (Nijmegen, The Netherlands) Observational Integration Theory with Applications to Riesz Spaces
Freitag	Zeichensaal, Mathematisches Institut, Wegelerstr. 10
15:00-15:50	Monika Seisenberger (Swansea, UK) Program Extraction from Proofs: Theory and Practice
16:00-16:50	Helmut Schwichtenberg (München) Logic for Computable Functionals and their Approximations
17:00-17:50	Thomas Streicher (Darmstadt) Shoenfield = Gödel after Krivine