Die Sommerschule richtete sich an Studierende der Mathematik, Philosophie, Informatik und anderer mathematik-naher Disziplinen mit Grundkenntnissen in Logik. Die Sommerschule vermittelte Einblicke in aktuelle Forschungsthemen in den Gebieten Logik und Berechenbarkeit. Das wissenschaftliche Programm bestand aus Minikursen (mit Vorlesungen, Übungen und Projekten), die durch einen historischen Exkurs ergänzt wurden.

Schedule zum Download (PDF), Liste der Projekte und Präsentationen

Minikurse



  • Gödels Unvollständigkeitssätze (Reinhard Kahle, Lissabon/Tübingen)
    Gödels Unvollständigkeitssätze sind in den Bereich der allgemeinen Mathematik einzuordnen. Sie beschäftigen sich mit der Nicht-Beweisbarkeit bestimmter formaler Aussagen. Ihr Verstehen ist hingegen oft durch philosophische und technische Ungenauigkeiten getrübt. Das Ziel dieses Kurses ist es, eine konzise Einführung in diese Ergebnisse, Beweise und deren Relevanz zu geben. Wir werden uns insbesondere mit der fundamentalen Unterscheidung zwischen Syntax und Semantik beschäftigen.


  • Rekursion und Komplexität (Isabel Oitavem, Lissabon)
    Die Berechenbarkeitstheorie liefert uns theoretische Ergebnisse davon, was berechnet werden kann. Nichtsdestotrotz kann nur ein Bruchteil der theoretisch berechenbaren Funktionen über effiziente Algorithmen implementiert werden. Die Komplexitätstheorie beschäftigt sich mit dieser Frage, normalerweise mithilfe von Automatenmodellen wie z. B. der Turingmaschine und expliziten Grenzen. Im Gegensatz dazu vermeiden implizite Beschreibungen von Komplexitätsklassen sowohl Automaten als auch explizite Komplexitätsbedingungen und erlauben daher eine mathematischere Beschreibung. In diesem Minikurs diskutieren wir verschiedene Beschreibungen von Komplexitätsklassen, die auf rekursiven Schemata beruhen.


  • Ordinalanalysis (Wolfram Pohlers, Münster)
    Aus Gödels Unvollständigkeitssätzen folgt, dass es kein Axiomensystem gibt, welches die Standardstruktur der natürlichen Zahlen beschreibt. Dasselbe gilt für andere Standardstrukturen, z. B. das konstruktible Mengenuniversum. Es ist anzumerken, dass Gödels Unvollständigkeitssatz nur die Existenz eines Theorems beweist, das in der Standardstruktur gilt, aber nicht innerhalb des Axiomensystems entschieden werden kann. Im Gegensatz dazu verfolgt die von Gentzen eingeführte Ordinalanalysis das Ziel, die "Anzahl der Transfinitness" eines gegebenen Axiomensystems zu ermitteln. Diese Anzahl kann in Form von transfiniten Ordinalzahlen erfasst werden. Dieser Minikurs ist als Einführung in unendliche Beweismethoden gedacht, die Unendlichkeitsrechnung auf Ordinalanalysis anwendet.


  • Automatisierte Beweisführung in der Automobilindustrie (Wolfgang Küchlin, Tübingen)
    In letzter Zeit wurden wichtige praktische Fortschritte in der Beweisführung des Boolean Satisfiability Solving (SAT-Solving) gemacht. Dies hat industrielle Anwendung ermöglicht, z. B. im Bereich der mikroelektronischen Leiterprüfung, Softwareverifizierung oder um Konfigurationsprobleme zu lösen. In diesem Kurs werden wir zuerst die algorithmischen Grundlagen aktueller SAT-Solver aufzeigen und daraufhin eine Einführung in Konfigurationsprobleme in der Automobilindustrie geben. Schließlich zeigen wir, wie man sie als SAT-Probleme formuliert und effizient löst. In diesem Beispiel werden Studierende die Anwendung von Logik im industriellen Kontext kennenlernen.


  • Hilbert and Bernays in Göttingen (Ulrich Stuhler, Göttingen)
    Göttingen ist der Ort, wo Hilbert und Bernays die Grundlagen der Arithmetik aufstellten. Ihre Zusammenarbeit gipfelte in dem zweibändigen Werk "Grundlagen der Mathematik". Dieser Kurs erinnert an diese historische Entwicklung.