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.
-------------------------------------------------------------------------