Praktikum Mathematische Logik (P2A1), Di 16-18, ab Mai 2018
"Praktische Formalisierungen mathematischer Beweise"

Aufgrund des Gödelschen Vollständigkeitssatzes und der Axiomatisierbarkeit der Mathematik in der Prädikatenlogik erster Stufe lassen sich mathematische Beweise als vollkommen formale Beweise in einem entsprechenden Kalkül ausführen. Formale Beweise interessanter Sätze werden allerdings sehr umfangreich und lassen sich nur mit Computerunterstützung beherrschen, wobei automatische Beweiser eingesetzt werden, um die üblichen Lücken mathematischer Texte zu überbrücken.

In dem Praktikum wollen grundlegende Algorithmen zur Verarbeitung von Logik aus dem "Handbook of Practical Logic and Automated Reasoning" von John Harrison kennenlernen. Diese sollen in Seminar-artigen Vorträgen vorgestellt werden. Parallel dazu werden wir uns in das "System for Automated Deduction" (SAD) einarbeiten, dass die Eingabe und Beweisüberprüfung von recht natürlich formulierten mathematischen Texten erlaubt. Ziel des Praktikums sind SAD-Formalisierungen umfangreicher Passagen aus Lehrbüchern.

Das Handbuch und SAD benutzen die funktionalen Programmiersprachen OCaml bzw. Haskell, die sich stark von den üblichen deklarativen Sprachen unterscheiden. Die selbständige Einarbeitung in diese Sprachen wird erwartet. Die Benutzung eines eigenen Laptops ist von Vorteil, ansonsten kann der Rechnerpool der Mathematik genutzt werden.

Das Praktikum trifft sich zu Vorträgen aus dem Handbook ab dem 29. Mai zum oben angegeben Termin. Die Praktikumsarbeiten (Formalisierungen oder auch Arbeiten am SAD-Code) werden Anfang Juli festgelegt. Da die Formalisierungen und Programmieraufgaben miteinander koordiniert werden müssen, ist die Teilnahme an mehreren, möglicherweise ganztägigen Koordinierungstreffen in den Semesterferien erforderlich.

Es werden ca. 12 Praktikumsplätze angeboten, bei großem Interesse wird es ein weiteres Praktikum im WS geben. Bewerbungen auf einen Platz müssen per Email an koepke@math.uni-bonn.de bis zum 5.5. geschickt werden. Bitte nennen Sie darin:
- Name
- Matr.-Nr.
- Email
- Studiengang
- Fachsemesterzahl
- sind Sie Hörer der jetzigen oder einer früheren Logikvorlesung?
- welche Übungsgruppe?
- in welchen Programmiersprachen besitzen Sie Programmiererfahrung?
- welche Wochen in der vorlesungsfreien Zeit bis Ende September sind Sie in
  Bonn (bitte in Kalenderwochen angeben)?
- ggf. weitere Bemerkungen

Die Zulassungen werden am Morgen des 7.5. mitgeteilt, und am 8.5., 16-18 gibt es ein erstes Treffen mit weiteren Informationen, Einteilungen usw.
-------------------------------------------------------------------------