Praktikum Mathematische Logik (P2A1), Do 10-12, N0.003, ab 7. November 2018
"Der Isabelle-Beweisprüfer"

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 werden wir mit dem bekannten Beweisassistenten "Isabelle" von L. Paulson und T. Nipkow arbeiten (https://isabelle.in.tum.de/). Das System soll zunächst in Seminar-artigen Vorträgen aus dem Buch "Isabelle/HOL, A Proof Assistant for Higher-Order Logic" (http://isabelle.in.tum.de/doc/tutorial.pdf) mit Vorführungen von Beispielen vorgestellt werden.

Als Praktikumsprojekte sind vor allem Formalisierungsaufgaben vorgesehen, die sich an vorhandenen Formalisierungen mit dem Bonner Beweissystem SAD3 (https://github.com/PeterKoepke/SAD3) orientieren. Die Projekte werden unmittelbar vor oder nach den Weihnachtsferien vergeben. Die Arbeiten sind bis Anfang März fertigzustellen.

Selbständiges Arbeiten mit Isabelle wird erwartet, insbesondere die Installation von Isabelle vor Beginn der Praktikumssitzungen. Eigene Laptops werden schon in der Seminarphase benötigt, um mit den vorgestellten Beispiele zu arbeiten. Ansonsten müssten Ersatzlösungen gefunden werden.

Es werden 8 - 10 Praktikumsplätze angeboten. Bewerbungen auf einen Platz müssen per Email an koepke@math.uni-bonn.de bis zum 31.10. 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? Kennen Sie Isabelle oder ein anderes Programm zur Beweisprüfung?
- ggf. weitere Bemerkungen

Die Zulassungen werden am 2.11.. mitgeteilt, und am 7.11., 10-12 gibt es ein erstes Treffen mit weiteren Informationen, Einteilungen usw.
-------------------------------------------------------------------------